Topological, automata-theoretic and logical characterization of finitary languages

K. Chatterjee, N. Fijalkow, Topological, Automata-Theoretic and Logical Characterization of Finitary Languages, IST Austria, 2010.

Download
OA 395.66 KB

Technical Report | Published | English
Author
;
Department
Series Title
IST Austria Technical Report
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 simplicity (abstraction 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 characterization of finitary languages defined by finitary parity and Streett conditions. We (a) show that the finitary parity and Streett languages are Σ2-complete; (b) present a complete characterization of the expressive power of various classes of automata with finitary and infinitary conditions (in particular we show that non-deterministic finitary parity and Streett automata cannot be determinized to deterministic finitary parity or Streett automata); and (c) show that the languages defined by non-deterministic finitary parity automata exactly characterize the star-free fragment of ωB-regular languages.
Publishing Year
Date Published
2010-06-04
Page
21
ISSN
IST-REx-ID

Cite this

Chatterjee K, Fijalkow N. Topological, Automata-Theoretic and Logical Characterization of Finitary Languages. IST Austria; 2010. doi:10.15479/AT:IST-2010-0002
Chatterjee, K., & Fijalkow, N. (2010). Topological, automata-theoretic and logical characterization of finitary languages. IST Austria. https://doi.org/10.15479/AT:IST-2010-0002
Chatterjee, Krishnendu, and Nathanaël Fijalkow. Topological, Automata-Theoretic and Logical Characterization of Finitary Languages. IST Austria, 2010. https://doi.org/10.15479/AT:IST-2010-0002.
K. Chatterjee and N. Fijalkow, Topological, automata-theoretic and logical characterization of finitary languages. IST Austria, 2010.
Chatterjee K, Fijalkow N. 2010. Topological, automata-theoretic and logical characterization of finitary languages, IST Austria, 21p.
Chatterjee, Krishnendu, and Nathanaël Fijalkow. Topological, Automata-Theoretic and Logical Characterization of Finitary Languages. IST Austria, 2010, doi:10.15479/AT:IST-2010-0002.
Main File(s)
Access Level
OA Open Access
Last Uploaded
2018-12-12T11:54:10Z


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar