R. Alur & S. La Torre (2004):
Deterministic Generators and Games for LTL Fragments.
ACM Transactions on Computational Logic (TOCL) 5(1),
pp. 1–15,
doi:10.1145/963927.963928.
R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger & B. Jobstmann (2010):
Robustness in the Presence of Liveness.
In: T. Touili, B. Cook & P. Jackson: Computer Aided Verification (CAV),
LNCS 6174.
Springer,
Edinburgh, UK,
pp. 410–424,
doi:10.1007/978-3-642-14295-6_36.
R. Bloem, A. Cimatti, K. Greimel, G. Hofferek, R. K\IeC önighofer, M. Roveri, V. Schuppan & R. Seeber (2010):
RATSY - A New Requirements Analysis Tool with Synthesis.
In: T. Touili, B. Cook & P. Jackson: Computer Aided Verification (CAV),
LNCS 6174.
Springer,
Edinburgh, UK,
pp. 425–429,
doi:10.1007/978-3-642-14295-6.
R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli & M. Weiglhofer (2007):
Automatic hardware synthesis from specifications: a case study.
In: R. Lauwereins & J. Madsen: Design, Automation and Test in Europe (DATE).
IEEE Computer Society,
Nice, France,
pp. 1188–1193.
R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli & M. Weiglhofer (2007):
Specify, Compile, Run: Hardware from PSL.
Electronic Notes in Theoretical Computer Science (ENTCS) 190,
pp. 3–16,
doi:10.1016/j.entcs.2007.09.004.
U. Boker & O. Kupferman (2009):
Co-ing B\IeC üchi Made Tight and Useful.
In: Logic in Computer Science (LICS).
IEEE Computer Society,
Los Angeles, California, USA,
pp. 245–254,
doi:10.1109/LICS.2009.32.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill & L.J. Hwang (1990):
Symbolic Model Checking: 10^20 States and Beyond.
In: Logic in Computer Science (LICS).
IEEE Computer Society,
Washington, DC, USA,
pp. 1–33,
doi:10.1109/LICS.1990.113767.
E.Y. Chang, Z. Manna & A. Pnueli (1992):
Characterization of Temporal Property Classes.
In: W. Kuich: International Colloquium on Automata, Languages and Programming (ICALP),
LNCS 623.
Springer,
Vienna, Austria,
pp. 474–486.
E.A. Emerson (1990):
Temporal and Modal Logic.
In: J. van Leeuwen: Handbook of Theoretical Computer Science, chapter 16 B: Formal Models and Semantics.
Elsevier,
pp. 995–1072.
C. Fritz (2005):
Simulation-Based Simplification of omega-Automata.
Technischen Fakult\IeC ät der Christian-Albrechts-Universit\IeC ät zu Kiel, Germany.
B. Jobstmann, S. Galler, M. Weiglhofer & R. Bloem (2007):
Anzu: A Tool for Property Synthesis.
In: W. Damm & H. Hermanns: Computer Aided Verification (CAV),
LNCS 4590.
Springer,
Berlin, Germany,
pp. 258–262,
doi:10.1007/978-3-540-73368-3_29.
O. Kupferman & M.Y. Vardi (1998):
Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time.
In: Logic in Computer Science (LICS).
IEEE Computer Society,
Indianapolis, Indiana, USA,
pp. 81–92,
doi:10.1109/LICS.1998.705645.
R. K\IeC önighofer, G. Hofferek & R. Bloem (2009):
Debugging formal specifications using simple counterstrategies.
In: Formal Methods in Computer-Aided Design (FMCAD).
IEEE Computer Society,
Austin, Texas, USA,
pp. 152–159,
doi:10.1109/FMCAD.2009.5351127.
M. Maidl (2000):
The Common Fragment of CTL and LTL.
In: Foundations of Computer Science (FOCS),
pp. 643–652.
Z. Manna & A. Pnueli (1987):
A Hierarchy of Temporal Properties.
In: Principles of Distributed Computing (PODC),
pp. 205,
doi:10.1145/41840.41857.
Z. Manna & A. Pnueli (1990):
A hierarchy of temporal properties.
In: Principles of Distributed Computing (PODC).
ACM,
Quebec City, Quebec, Canada,
pp. 377–408.
Z. Manna & A. Pnueli (1991):
Completing the temporal picture.
Theoretical Computer Science (TCS) 83(1),
pp. 97–130,
doi:10.1016/0304-3975(91)90041-Y.
S. Miyano & T. Hayashi (1984):
Alternating automata on ω-words.
Theoretical Computer Science (TCS) 32,
pp. 321–330,
doi:10.1016/0304-3975(84)90049-5.
A. Morgenstern, K. Schneider & S. Lamberti (2008):
Generating Deterministic ω-Automata for most LTL Formulas by the Breakpoint Construction.
In: C. Scholl & S. Disch: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV).
Shaker,
Freiburg, Germany,
pp. 119–128.
N. Piterman, A. Pnueli & Y. Sa\IeC ar (2006):
Synthesis of Reactive(1) Designs.
In: E.A. Emerson & K.S. Namjoshi: Verification, Model Checking, and Abstract Interpretation (VMCAI),
LNCS 3855.
Springer,
Charleston, South Carolina, USA,
pp. 364–380,
doi:10.1007/11609773_24.
A. Pnueli (1977):
The Temporal Logic of Programs.
In: Foundations of Computer Science (FOCS).
IEEE Computer Society,
Providence, Rhode Island, USA,
pp. 46–57,
doi:10.1109/SFCS.1977.32.
K. Schneider (2001):
Improving Automata Generation for Linear Temporal Logic by Considering the Automata Hierarchy.
In: R. Nieuwenhuis & A. Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR),
LNAI 2250.
Springer,
Havana, Cuba,
pp. 39–54,
doi:10.1007/3-540-45653-8_3.
K. Schneider (2003):
Verification of Reactive Systems - Formal Methods and Algorithms.
Texts in Theoretical Computer Science (EATCS Series).
Springer.
K. Schneider (2009):
The Synchronous Programming Language Quartz.
Internal Report 375.
Department of Computer Science, University of Kaiserslautern,
Kaiserslautern, Germany.
W. Thomas (1990):
Automata on Infinite Objects.
In: J. van Leeuwen: Handbook of Theoretical Computer Science, chapter 4 B: Formal Models and Semantics.
Elsevier,
pp. 133–191.
K. Wagner (1979):
On ω-regular sets.
Information and Control 43(2),
pp. 123–177.
N. Wallmeier, P. H\IeC ütten & W. Thomas (2003):
Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications.
In: O.H. Ibarra & Z. Dang: Conference on Implementation and Application of Automata (CIAA),
LNCS 2759.
Springer,
Santa Barbara, California, USA,
pp. 11–22,
doi:10.1007/3-540-45089-0_3.
T. Wongpiromsarn, U. Topcu & R.M. Murray (2010):
Receding horizon control for temporal logic specifications.
In: K.H. Johansson & W. Yi: Hybrid Systems: Computation and Control (HSCC).
ACM,
Stockholm, Sweden,
pp. 101–110,
doi:10.1145/1755952.1755968.
eptcs@eptcs.org