Finitary languages

8 years 8 months ago
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...
Krishnendu Chatterjee, Nathanaël Fijalkow
Added 13 May 2011
Updated 13 May 2011
Type Journal
Year 2011
Where CORR
Authors Krishnendu Chatterjee, Nathanaël Fijalkow
Comments (0)