Finitary languages

Abstract The class of ω-regular languages provide a robust specification language in verification. Every ω-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplictraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider the finitary parity and Streett (fairness) conditions. We present the topological, automata-theoretic and logical characteriz...

• Type: Journal
• Year: 2011
• Where: CORR
• Authors: Krishnendu Chatterjee, Nathanaël Fijalkow
• Keywords: CORR 2011, Education, Non-deterministic finitary Parity, Streett Automata, finitary Parity