2020/02/20 by Christian Herrera, Herrera, Christian
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Software Reliability and Analysis Research #Software Testing and Debugging Techniques #cs.FL #cs.LO
paper · pdf · doi:10.48550/arxiv.2002.08646
arxiv created 2020/02/20 · openalex publication_date 2020/02/20 · arxiv updated 2020/02/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present the notion of stateful priorities for imposing precise restrictions on system actions, in order to meet safety constraints. By using stateful priorities we are able to exclusively restrict erroneous system behavior as specified by the constraint, whereas safe system behavior remains unrestricted. Given a system modeled as a network of discrete automata and an error constraint, we present algorithms which use those inputs to synthesize stateful priorities. We present as well a network transformation which uses synthesized priorities for blocking all system actions leading to the input error. Our experiments with three real-world examples demonstrate the applicability of our approach.