Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(8)
Decision Procedure
Finite State Automata
Infinite Word
Model Checking
Monadic Second Order Logic
Satisfiability
Computation Tree Logic
Linear Time Temporal Logic
Subscribe
Academic
Publications
Automata: from logics to algorithms
Automata: from logics to algorithms,Moshe Y. Vardi,Thomas Wilke
Edit
Automata: from logics to algorithms
(
Citations: 7
)
BibTex

RIS

RefWorks
Download
Moshe Y. Vardi
,
Thomas Wilke
We review, in a unified framework, translations from five dif ferent logics—monadic secondorder logic of one and two successors (S1S and S2S), lineartime
temporal logic
(LTL),
computation tree logic
(CTL), and modal µcalculus (MC)—into appropriate models of finitestate automata on infinite words or infinite trees. Together with emptinesstesting algorithms for these models of automata, this yields decision procedures for these logics. The translations are presented in a modular fashion and in a way such that optimal complexity bounds for satisfiability, conformance (model checking), and realizability are obtained for all logics.
Published in 2008.
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.informatik.unitrier.de
)
Citation Context
(4)
...Ramseybased approach [3,22], determinizationbased approach [20,18,2,19], rankbased approach [24,15,13], and slicebased approach [10,
30
]...
...The blowup of the construction is 4(3n) n while its preliminary version in [
30
], referred to as Slice here, has a (3n) n blowup 1 . Unlike...
MingHsien Tsai
,
et al.
State of Büchi Complementation
...A preliminary version of the complementation construction presented here was described in [
20
]...
...The exposition in the present paper is more modular, in particular, [
20
] did not have the intermediate slice automaton, which is the basis for both complementation and disambiguation...
Detlef Kähler
,
et al.
Complementation, Disambiguation, and Determinization of Büchi Automata...
...Finite automata have emerged with several modern applications, e.g., optimization of logic based programs and specification and verification of protocols [
21
]...
Nabeel Sabir
,
et al.
Linking Finite Automata and Formal Methods Enhancing Modeling Power fo...
...We translate ψ to a deterministic parity word automaton using a standard construction (cf. [
8
]). � 22 W. Damm and B. Finkbeiner...
Werner Damm
,
et al.
Does It Pay to Extend the Perimeter of a World Model?
References
(118)
The ForSpec Temporal Logic: A New Temporal PropertySpecification Language
(
Citations: 110
)
Roy Armoni
,
Limor Fix
,
Alon Flaisher
,
Rob Gerth
,
Boris Ginsburg
,
Tomer Kanza
,
Avner Landver
,
Sela Madorhaim
,
Eli Singerman
,
Andreas Tiemeyer
,
Moshe Y. Vardi
,
Yael Zbar
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 296211, 2002
Deterministic Dynamic Monitors for LinearTime Assertions
(
Citations: 13
)
Roy Armoni
,
Dmitry Korchemny
,
Andreas Tiemeyer
,
Moshe Y. Vardi
,
Yael Zbar
Conference:
International Workshop on Formal Approaches to Testing of Software  FATES/RV
, pp. 163177, 2006
Rudiments of mucalculus
(
Citations: 74
)
A. Arnold
Published in 2001.
Rational omegaLanguages are NonAmbiguous
(
Citations: 9
)
André Arnold
Journal:
Theoretical Computer Science  TCS
, vol. 26, pp. 221223, 1983
Observations on Determinization of Büchi Automata
(
Citations: 16
)
Christoph Schulte Althoff
,
Wolfgang Thomas
,
Nico Wallmeier
Conference:
Workshop on Implementing Automata/Conference on Implementation and Application of Automata  CIAA(WIA)
, pp. 262272, 2005
Sort by:
Citations
(7)
Qualitative Tree Languages
Arnaud Carayol
,
Axel Haddad
,
Olivier Serre
Conference:
Logic in Computer Science  LICS
, pp. 1322, 2011
State of Büchi Complementation
MingHsien Tsai
,
Seth Fogarty
,
Moshe Y. Vardi
,
YihKuen Tsay
Conference:
Workshop on Implementing Automata/Conference on Implementation and Application of Automata  CIAA(WIA)
, pp. 261271, 2010
Games and logic (Parity games)
Igor Walukiewicz
Published in 2009.
Complementation, Disambiguation, and Determinization of Büchi Automata Unified
(
Citations: 12
)
Detlef Kähler
,
Thomas Wilke
Conference:
International Colloquium on Automata, Languages and Programming  ICALP
, pp. 724735, 2008
Construction of Intersection of Nondeterministic Finite Automata using Z Notation
(
Citations: 4
)
Nazir Ahmad Zafar
,
Nabeel Sabir
,
Amir Ali
Published in 2008.