Ranking Automata and Games for Prioritized Requirements

Requirements of reactive systems are usually specified by classifying system executions as desirable and undesirable. To specify prioritized requirements, we propose to associate a rank with each execution. This leads to optimization analogs of verification and synthesis problems in which we compute the "best" requirement that can be satisfied or enforced from a given state. The classical definitions of acceptance criteria for automata can be generalized to ranking conditions. In particular, given a mapping of states to colors, the B

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Rajeev Alur, Aditya Kanade, Gera Weiss
• Keywords: CAV 2008, Cyclic Ranking, Cyclic Ranking Condition, Hardware, Ranking Conditions