From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata

Nir Piterman

doi:10.2168/LMCS-3(3:5)2007

Nir Piterman - From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata

lmcs:1199 - Logical Methods in Computer Science, August 14, 2007, Volume 3, Issue 3 - https://doi.org/10.2168/LMCS-3(3:5)2007

From Nondeterministic Büchi and Streett Automata to Deterministic Parity AutomataArticle

Authors: Nir Piterman

In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).

Comment: 21 pages. To appear in Logical Methods in Computer Science (LMCS)

https://doi.org/10.2168/LMCS-3(3:5)2007

Source: arXiv.org:0705.2205

Volume: Volume 3, Issue 3

Secondary volumes: Selected Papers of the 21st IEEE Symposium on Logic in Computer Science (LICS 2006)

Published on: August 14, 2007

Imported on: November 9, 2006

Keywords: Computer Science - Logic in Computer Science, Computer Science - Formal Languages and Automata Theory, F.1.1, F.4.3

Licence: arXiv.org - Assumed non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

103 Documents citing this article

Giuseppe De Giacomo;Giuseppe Perelli, 2025, Behavioral QLTL, Autonomous Agents and Multi-Agent Systems, 39, 2, 10.1007/s10458-025-09712-w.

Philippe Heim;Rayna Dimitrova, 2025, Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis, Proceedings of the ACM on Programming Languages, 9, POPL, pp. 1536-1567, 10.1145/3704888, https://doi.org/10.1145/3704888.

Raven Beutner;Bernd Finkbeiner, 2025, AutoHyper: leveraging language inclusion checking for hyperproperty model-checking, International Journal on Software Tools for Technology Transfer, 10.1007/s10009-025-00801-5, https://doi.org/10.1007/s10009-025-00801-5.

Francesco Belardinelli;Ioana Boureanu;Catalin Dima;Vadim Malvone, 2024, Model-checking Strategic Abilities in Information-sharing Systems, ACM Transactions on Computational Logic, 26, 1, pp. 1-45, 10.1145/3704919, https://doi.org/10.1145/3704919.

Swen Jacobs;Guillermo A. Pérez;Remco Abraham;Véronique Bruyère;Michaël Cadilhac;et al., 2024, The Reactive Synthesis Competition (SYNTCOMP): 2018–2021, University of Twente Research Information, 26, 5, pp. 551-567, 10.1007/s10009-024-00754-1, https://research.utwente.nl/en/publications/d0fa5204-4615-49a2-a484-69be1ce2369a.

Michaël Cadilhac;Guillermo A. Pérez, 2023, Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability, Lecture notes in computer science, pp. 192-207, 10.1007/978-3-031-30820-8_14, https://doi.org/10.1007/978-3-031-30820-8_14.

Patricia Bouyer;Orna Kupferman;Nicolas Markey;Bastien Maubert;Aniello Murano;Giuseppe Perelli, 2023, Reasoning about Quality and Fuzziness of Strategic Behaviors, SPIRE - Sciences Po Institutional REpository, 24, 3, pp. 1-38, 10.1145/3582498, https://inria.hal.science/hal-04219131.

Raven Beutner;Bernd Finkbeiner, 2023, AutoHyper: Explicit-State Model Checking for HyperLTL, Lecture notes in computer science, pp. 145-163, 10.1007/978-3-031-30823-9_8, https://doi.org/10.1007/978-3-031-30823-9_8.

Vojtěch Havlena;Ondřej Lengál;Yong Li;Barbora Šmahlíková;Andrea Turrini, 2023, Modular Mix-and-Match Complementation of Büchi Automata, Lecture notes in computer science, pp. 249-270, 10.1007/978-3-031-30823-9_13, https://doi.org/10.1007/978-3-031-30823-9_13.

Andrea Turrini, 2022, An Introduction to Quantum Model Checking, Applied Sciences, 12, 4, pp. 2016, 10.3390/app12042016, https://doi.org/10.3390/app12042016.

Chen Fu;Ernst Moritz Hahn;Yong Li;Sven Schewe;Meng Sun;et al., 2022, EPMC Gets Knowledge in Multi-agent Systems, University of Twente Research Information, pp. 93-107, 10.1007/978-3-030-94583-1_5, https://research.utwente.nl/en/publications/830473c7-f2bd-4820-a300-a279e50886ea.

Daniel Hausmann;Nir Piterman, 2022, A Survey on Satisfiability Checking for the $$\mu $$-Calculus Through Tree Automata, Lecture notes in computer science, pp. 228-251, 10.1007/978-3-031-22337-2_11.

Javier Esparza;Jan Křetínský;Jean-François Raskin;Salomon Sickert, 2022, From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata, International Journal on Software Tools for Technology Transfer, 24, 4, pp. 635-659, 10.1007/s10009-022-00663-1, https://doi.org/10.1007/s10009-022-00663-1.

Kyveli Doveri;Pierre Ganty;Nicolas Mazzocchi, 2022, FORQ-Based Language Inclusion Formal Testing, Lecture notes in computer science, pp. 109-129, 10.1007/978-3-031-13188-2_6, https://doi.org/10.1007/978-3-031-13188-2_6.

Vojtěch Havlena;Ondřej Lengál;Barbora Šmahlíková, 2022, Complementing Büchi Automata with Ranker, Lecture notes in computer science, pp. 188-201, 10.1007/978-3-031-13188-2_10, https://doi.org/10.1007/978-3-031-13188-2_10.

Vojtěch Havlena;Ondřej Lengál;Barbora Šmahlíková, 2022, Sky Is Not the Limit, Lecture notes in computer science, pp. 118-136, 10.1007/978-3-030-99527-0_7, https://doi.org/10.1007/978-3-030-99527-0_7.

Yong Li;Andrea Turrini;Weizhi Feng;Moshe Y. Vardi;Lijun Zhang, 2022, Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition, Lecture notes in computer science, pp. 152-173, 10.1007/978-3-031-13188-2_8, https://doi.org/10.1007/978-3-031-13188-2_8.

Alessandro Abate;Julian Gutierrez;Lewis Hammond;Paul Harrenstein;Marta Kwiatkowska;et al., 2021, Rational verification: game-theoretic verification of multi-agent systems, Applied Intelligence, 51, 9, pp. 6569-6584, 10.1007/s10489-021-02658-y, https://doi.org/10.1007/s10489-021-02658-y.

Bohn, Leon;Löding, Christof, 2021, Constructing Deterministic ω-Automata from Examples by an Extension of the RPNI Algorithm, RWTH Publications (RWTH Aachen), 10.18154/rwth-2022-01667, https://doi.org/10.18154/rwth-2022-01667.

Clemens Kupke;Johannes Marti;Yde Venema, 2021, On the size of disjunctive formulas in the μ-calculus, Electronic Proceedings in Theoretical Computer Science, 346, pp. 291-307, 10.4204/eptcs.346.19, https://doi.org/10.4204/eptcs.346.19.

Doveri, Kyveli;Ganty, Pierre;Parolini, Francesco;Ranzato, Francesco, 2021, Inclusion Testing of Büchi Automata Based on Well-Quasiorders, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), pp. 22-, 10.4230/lipics.concur.2021.3, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.3.

Kiefer, Stefan;Semukhin, Pavel;Widdershoven, Cas, 2021, Linear-Time Model Checking Branching Processes, arXiv (Cornell University), 10.4230/lipics.concur.2021.6, http://arxiv.org/abs/2107.01687.

Liping Xiong;Sumei Guo, 2021, Representation and Reasoning about Strategic Abilities with ω-Regular Properties, Mathematics, 9, 23, pp. 3052, 10.3390/math9233052, https://doi.org/10.3390/math9233052.

Lucas M. Tabajara;Moshe Y. Vardi, 2021, Linear Temporal Logic – From Infinite to Finite Horizon, Lecture notes in computer science, pp. 3-12, 10.1007/978-3-030-88885-5_1.

Vojtěch Havlena;Ondřej Lengál;Barbora Šmahlíková, 2021, Deciding S1S: Down the Rabbit Hole and Through the Looking Glass, Lecture notes in computer science, pp. 215-222, 10.1007/978-3-030-91014-3_15.

Cong Tian;Wensheng Wang;Zhenhua Duan, 2020, Making Streett Determinization Tight, Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 859-872, 10.1145/3373718.3394757.

Cristian S. Calude;Sanjay Jain;Bakhadyr Khoussainov;Wei Li;Frank Stephan, 2020, Deciding Parity Games in Quasi-polynomial Time, SIAM Journal on Computing, 51, 2, pp. STOC17-152, 10.1137/17m1145288.

Ernst Moritz Hahn;Mateo Perez;Sven Schewe;Fabio Somenzi;Ashutosh Trivedi;Dominik Wojtczak, 2020, Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning, Lecture notes in computer science, pp. 306-323, 10.1007/978-3-030-45190-5_17, https://doi.org/10.1007/978-3-030-45190-5_17.

František Blahoudek;Alexandre Duret-Lutz;Jan Strejček, 2020, Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization, Lecture notes in computer science, pp. 15-27, 10.1007/978-3-030-53291-8_2, https://doi.org/10.1007/978-3-030-53291-8_2.

Javier Esparza;Jan Křetínský;Salomon Sickert, 2020, A Unified Translation of Linear Temporal Logic to ω-Automata, Journal of the ACM, 67, 6, pp. 1-61, 10.1145/3417995, https://doi.org/10.1145/3417995.

Julian Gutierrez;Aniello Murano;Giuseppe Perelli;Sasha Rubin;Thomas Steeples;Michael Wooldridge, 2020, Equilibria for games with combined qualitative and quantitative objectives, IRIS Research product catalog (Sapienza University of Rome), 58, 6, pp. 585-610, 10.1007/s00236-020-00385-4, http://hdl.handle.net/11573/1418258.

Julian Gutierrez;Muhammad Najib;Giuseppe Perelli;Michael Wooldridge, 2020, Automated temporal equilibrium analysis: Verification and synthesis of multi-player games, IRIS Research product catalog (Sapienza University of Rome), 287, pp. 103353, 10.1016/j.artint.2020.103353, http://hdl.handle.net/11573/1422753.

Christof Löding;Anton Pirogov, 2019, New Optimizations and Heuristics for Determinization of Büchi Automata, arXiv (Cornell University), pp. 317-333, 10.1007/978-3-030-31784-3_18, http://arxiv.org/abs/1911.01759.

Jan Křetínský;Alexander Manta;Tobias Meggendorfer, 2019, Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis, arXiv (Cornell University), pp. 404-422, 10.1007/978-3-030-31784-3_24, http://arxiv.org/abs/1907.12157.

John Fearnley;Sanjay Jain;Bart de Keijzer;Sven Schewe;Frank Stephan;Dominik Wojtczak, 2019, An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space, International Journal on Software Tools for Technology Transfer, 21, 3, pp. 325-349, 10.1007/s10009-019-00509-3.

Udi Boker, 2019, Inherent Size Blowup in $$\omega $$ -Automata, Lecture notes in computer science, pp. 3-17, 10.1007/978-3-030-24886-4_1.

Yong Li;Andrea Turrini;Yu-Fang Chen;Lijun Zhang, 2019, Learning Büchi Automata and Its Applications, Lecture notes in computer science, pp. 38-98, 10.1007/978-3-030-17601-3_2.

Yong Li;Xuechao Sun;Andrea Turrini;Yu-Fang Chen;Junnan Xu, 2019, ROLL 1.0: $$\omega $$ -Regular Language Learning Library, Lecture notes in computer science, pp. 365-371, 10.1007/978-3-030-17462-0_23, https://doi.org/10.1007/978-3-030-17462-0_23.

Yu-Fang Chen;Vojtěch Havlena;Ondřej Lengál, 2019, Simulations in Rank-Based Büchi Automata Complementation, arXiv (Cornell University), pp. 447-467, 10.1007/978-3-030-34175-6_23, https://arxiv.org/abs/1905.07139v1.

Daniel Hausmann;Lutz Schröder;Hans-Peter Deifel, 2018, Permutation Games for the Weakly Aconjunctive $$\mu $$ μ -Calculus, Lecture notes in computer science, pp. 361-378, 10.1007/978-3-319-89963-3_21, https://doi.org/10.1007/978-3-319-89963-3_21.

Julian Bradfield;Igor Walukiewicz, 2018, The mu-calculus and Model Checking, pp. 871-919, 10.1007/978-3-319-10575-8_26, https://hal.science/hal-02397703.

Orna Kupferman, 2018, Automata Theory and Model Checking, Handbook of Model Checking, pp. 107-151, 10.1007/978-3-319-10575-8_4.

Ayrat Khalimov;Roderick Bloem, 2017, Bounded Synthesis for Streett, Rabin, and $$\text {CTL}^{*}$$, Lecture notes in computer science, pp. 333-352, 10.1007/978-3-319-63390-9_18.

Béatrice Bérard;Olga Kouchnarenko;John Mullins;Mathieu Sassolas, 2017, Opacity for linear constraint Markov chains, 28, 1, pp. 83-108, 10.1007/s10626-017-0259-4, https://hal.sorbonne-universite.fr/hal-01384153.

Cristian S. Calude;Sanjay Jain;Bakhadyr Khoussainov;Wei Li;Frank Stephan, 2017, Deciding parity games in quasipolynomial time, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, pp. 252-263, 10.1145/3055399.3055409.

Jan Křetínský;Tobias Meggendorfer;Clara Waldmann;Maximilian Weininger, 2017, Index Appearance Record for Transforming Rabin Automata into Parity Automata, arXiv (Cornell University), pp. 443-460, 10.1007/978-3-662-54577-5_26, http://arxiv.org/abs/1701.05738.

Javier Esparza;Jan Křetínský;Jean-François Raskin;Salomon Sickert, 2017, From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata, arXiv (Cornell University), pp. 426-442, 10.1007/978-3-662-54577-5_25, http://arxiv.org/abs/1701.06103.

Orna Kupferman;Gal Vardi, 2017, On relative and probabilistic finite counterability, Formal Methods in System Design, 52, 2, pp. 117-146, 10.1007/s10703-017-0277-8.

Paul Hunter;Guillermo A. Pérez;Jean-François Raskin, 2017, Looking at mean payoff through foggy windows, Acta Informatica, 55, 8, pp. 627-647, 10.1007/s00236-017-0304-7, https://doi.org/10.1007/s00236-017-0304-7.

Yusi Lei;Fu Song;Wanwei Liu;Min Zhang, 2017, On the complexity of ω-pushdown automata, Science China Information Sciences, 60, 11, 10.1007/s11432-016-9026-x.

Amina Doumane;David Baelde;Lucca Hirschi;Alexis Saurin, 2016, Towards Completeness via Proof Search in the Linear Time μ-calculus, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 377-386, 10.1145/2933575.2933598.

Beatrice Berard;Olga Kouchnarenko;John Mullins;Mathieu Sassolas, 2016, Preserving opacity on Interval Markov Chains under simulation, 44, pp. 319-324, 10.1109/wodes.2016.7497866.

Bernd Finkbeiner;Felix Klein, 2016, Bounded Cycle Synthesis, Lecture notes in computer science, pp. 118-135, 10.1007/978-3-319-41528-4_7.

Dana Fisman, 2016, A Complexity Measure on Büchi Automata, Lecture notes in computer science, pp. 102-113, 10.1007/978-3-319-30000-9_8.

František Blahoudek;Matthias Heizmann;Sven Schewe;Jan Strejček;Ming-Hsien Tsai, 2016, Complementing Semi-deterministic Büchi Automata, Lecture notes in computer science, pp. 770-787, 10.1007/978-3-662-49674-9_49.

Krishnendu Chatterjee;Laurent Doyen;Emmanuel Filiot;Jean-François Raskin, 2016, Doomsday equilibria for omega-regular games, Information and Computation, 254, pp. 296-315, 10.1016/j.ic.2016.10.012.

Paul Hunter;Guillermo A. Pérez;Jean-François Raskin, 2016, Reactive synthesis without regret, Acta Informatica, 54, 1, pp. 3-39, 10.1007/s00236-016-0268-z, https://doi.org/10.1007/s00236-016-0268-z.

Ruediger Ehlers;Salar Moarref;Ufuk Topcu, 2016, Risk-averse control of Markov decision processes with ω-regular objectives, 2016 IEEE 55th Conference on Decision and Control (CDC), pp. 426-433, 10.1109/cdc.2016.7798306.

Salomon Sickert;Javier Esparza;Stefan Jaax;Jan Křetínský, 2016, Limit-Deterministic Büchi Automata for Linear Temporal Logic, Lecture notes in computer science, pp. 312-332, 10.1007/978-3-319-41540-6_17.

Souymodip Chakraborty;Joost-Pieter Katoen, 2016, On the Satisfiability of Some Simple Probabilistic Logics, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 56-65, 10.1145/2933575.2934526.

Sven Schewe, 2016, Solving parity games in big steps, Journal of Computer and System Sciences, 84, pp. 243-262, 10.1016/j.jcss.2016.10.002.

Christian von Essen;Barbara Jobstmann, 2015, Program repair without regret, Infoscience (Ecole Polytechnique Fédérale de Lausanne), 47, 1, pp. 26-50, 10.1007/s10703-015-0223-6, https://infoscience.epfl.ch/handle/20.500.14299/176106.

Farn Wang;Sven Schewe;Chung-Hao Huang, 2015, An Extension of ATL with Strategy Interaction, ACM Transactions on Programming Languages and Systems, 37, 3, pp. 1-41, 10.1145/2734117, https://doi.org/10.1145/2734117.

Mária Svoreňová;Martin Chmelík;Kevin Leahy;Hasan Ferit Eniser;Krishnendu Chatterjee;et al., 2015, Temporal logic motion planning using POMDPs with parity objectives, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 233-238, 10.1145/2728606.2728617.

Oliver Friedmann;Felix Klaedtke;Martin Lange, 2015, Ramsey-Based Inclusion Checking for Visibly Pushdown Automata, ACM Transactions on Computational Logic, 16, 4, pp. 1-24, 10.1145/2774221.

Paul Hunter;Guillermo A. Pérez;Jean-François Raskin, 2015, Looking at Mean-Payoff Through Foggy Windows, Lecture notes in computer science, pp. 429-445, 10.1007/978-3-319-24953-7_31.

Rachel Faran;Orna Kupferman, 2015, Spanning the Spectrum from Safety to Liveness, Lecture notes in computer science, pp. 183-200, 10.1007/978-3-319-24953-7_13.

Steen Vester, 2015, On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems, Lecture notes in computer science, pp. 361-377, 10.1007/978-3-319-24953-7_27.

Sven Schewe;Ashutosh Trivedi;Thomas Varghese, 2015, Symmetric Strategy Improvement, Lecture notes in computer science, pp. 388-400, 10.1007/978-3-662-47666-6_31.

Jérémie Cabessa;Alessandro E. P. Villa, 2014, An Attractor-Based Complexity Measurement for Boolean Recurrent Neural Networks, PLoS ONE, 9, 4, pp. e94204, 10.1371/journal.pone.0094204, https://doi.org/10.1371/journal.pone.0094204.

Krishnendu Chatterjee;Laurent Doyen;Emmanuel Filiot;Jean-François Raskin, 2014, Doomsday Equilibria for Omega-Regular Games, Lecture notes in computer science, pp. 78-97, 10.1007/978-3-642-54013-4_5.

Shaull Almagor;Orna Kupferman, 2014, Latticed-LTL Synthesis in the Presence of Noisy Inputs, Lecture notes in computer science, pp. 226-241, 10.1007/978-3-642-54830-7_15, https://doi.org/10.1007/978-3-642-54830-7_15.

Sven Schewe;Thomas Varghese, 2014, Determinising Parity Automata, arXiv (Cornell University), pp. 486-498, 10.1007/978-3-662-44522-8_41, http://arxiv.org/abs/1401.5394.

Sven Schewe;Thomas Varghese, 2014, Tight Bounds for Complementing Parity Automata, arXiv (Cornell University), pp. 499-510, 10.1007/978-3-662-44522-8_42, http://arxiv.org/abs/1406.1090.

Zuzana Komárková;Jan Křetínský, 2014, Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata, Lecture notes in computer science, pp. 235-241, 10.1007/978-3-319-11936-6_17.

Christian von Essen;Barbara Jobstmann, 2013, Program Repair without Regret, Lecture notes in computer science, pp. 896-911, 10.1007/978-3-642-39799-8_64, https://doi.org/10.1007/978-3-642-39799-8_64.

Cong Tian;Zhenhua Duan;Mengfei Yang, 2013, Deternimization of Büchi Automata as Partitioned Automata, Lecture notes in computer science, pp. 158-168, 10.1007/978-3-642-38768-5_16.

František Blahoudek;Mojmír Křetínský;Jan Strejček, 2013, Comparison of LTL to Deterministic Rabin Automata Translators, Lecture notes in computer science, pp. 164-172, 10.1007/978-3-642-45221-5_12.

Krishnendu Chatterjee;Andreas Gaiser;Jan Křetínský, 2013, Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis, Lecture notes in computer science, pp. 559-575, 10.1007/978-3-642-39799-8_37, https://doi.org/10.1007/978-3-642-39799-8_37.

Nir Piterman, 2013, Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development, Lecture notes in computer science, pp. 45-49, 10.1007/978-3-642-40313-2_6.

Rastislav Bodik;Barbara Jobstmann, 2013, Algorithmic program synthesis: introduction, International Journal on Software Tools for Technology Transfer, 15, 5-6, pp. 397-411, 10.1007/s10009-013-0287-9.

Seth Fogarty;Orna Kupferman;Moshe Y. Vardi;Thomas Wilke, 2013, Profile Trees for Büchi Word Automata, with Application to Determinization, Electronic Proceedings in Theoretical Computer Science, 119, pp. 107-121, 10.4204/eptcs.119.11, https://doi.org/10.4204/eptcs.119.11.

Tomáš Babiak;František Blahoudek;Mojmír Křetínský;Jan Strejček, 2013, Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment, Lecture notes in computer science, pp. 24-39, 10.1007/978-3-319-02444-8_4.

Jan Křetínský;Javier Esparza, 2012, Deterministic Automata for the (F,G)-Fragment of LTL, Lecture notes in computer science, pp. 7-22, 10.1007/978-3-642-31424-7_7.

Orna Kupferman, 2012, Recent Challenges and Ideas in Temporal Synthesis, Lecture notes in computer science, pp. 88-98, 10.1007/978-3-642-27660-6_8.

Orna Kupferman;Dorsa Sadigh;Sanjit A. Seshia, 2012, Synthesis with Clairvoyance, Lecture notes in computer science, pp. 5-19, 10.1007/978-3-642-34188-5_5.

Saqib Sohail;Fabio Somenzi, 2012, Safety first: a two-stage algorithm for the synthesis of reactive systems, International Journal on Software Tools for Technology Transfer, 15, 5-6, pp. 433-454, 10.1007/s10009-012-0224-3.

Stefan Breuers;Christof Löding;Jörg Olschewski, 2012, Improved Ramsey-Based Büchi Complementation, Lecture notes in computer science, pp. 150-164, 10.1007/978-3-642-28729-9_10.

Sven Schewe;Thomas Varghese, 2012, Tight Bounds for the Determinisation and Complementation of Generalised Büchi Automata, Lecture notes in computer science, pp. 42-56, 10.1007/978-3-642-33386-6_5.

Emmanuel Filiot;Naiyong Jin;Jean-François Raskin, 2011, Antichains and compositional algorithms for LTL synthesis, Formal Methods in System Design, 39, 3, pp. 261-296, 10.1007/s10703-011-0115-3.

Rüdiger Ehlers, 2011, Symbolic bounded synthesis, Formal Methods in System Design, 40, 2, pp. 232-262, 10.1007/s10703-011-0137-x.

Rüdiger Ehlers;Bernd Finkbeiner, 2011, Reactive Safety, Electronic Proceedings in Theoretical Computer Science, 54, pp. 178-191, 10.4204/eptcs.54.13, https://doi.org/10.4204/eptcs.54.13.

Barbara Di Giampaolo;Gilles Geeraerts;Jean-François Raskin;Nathalie Sznajder, 2010, Safraless Procedures for Timed Specifications, Lecture notes in computer science, pp. 2-22, 10.1007/978-3-642-15297-9_2.

Orna Kupferman;Moshe Y. Vardi, 2010, Synthesis of Trigger Properties, Lecture notes in computer science, pp. 312-331, 10.1007/978-3-642-17511-4_18.

Patrice Godefroid;Nir Piterman, 2010, LTL generalized model checking revisited, International Journal on Software Tools for Technology Transfer, 13, 6, pp. 571-584, 10.1007/s10009-010-0169-3.

Emmanuel Filiot;Naiyong Jin;Jean-François Raskin, 2009, An Antichain Algorithm for LTL Realizability, Lecture notes in computer science, pp. 263-277, 10.1007/978-3-642-02658-4_22, https://doi.org/10.1007/978-3-642-02658-4_22.

Laurent Doyen;Gilles Geeraerts;Jean-Francois Raskin;Julien Reichert, 2009, Realizability of Real-Time Logics, Lecture notes in computer science, pp. 133-148, 10.1007/978-3-642-04368-0_12.

Sven Schewe, 2009, Tighter Bounds for the Determinisation of Büchi Automata, Lecture notes in computer science, pp. 167-181, 10.1007/978-3-642-00596-1_13.

Sven Schewe, 2009, From Parity and Payoff Games to Linear Programming, Lecture notes in computer science, pp. 675-686, 10.1007/978-3-642-03816-7_57.

Thomas Colcombet;Konrad Zdanowski, 2009, A Tight Lower Bound for Determinization of Transition Labeled Büchi Automata, Lecture notes in computer science, pp. 151-162, 10.1007/978-3-642-02930-1_13.

Karin Greimel;Roderick Bloem;Barbara Jobstmann;Moshe Vardi, 2008, Open Implication, Lecture notes in computer science, pp. 361-372, 10.1007/978-3-540-70583-3_30.

Patrice Godefroid;Nir Piterman, 2008, LTL Generalized Model Checking Revisited, Lecture notes in computer science, pp. 89-104, 10.1007/978-3-540-93900-9_11.

Orna Kupferman;Nir Piterman;Moshe Y. Vardi, 2006, Safraless Compositional Synthesis, Lecture notes in computer science, pp. 31-44, 10.1007/11817963_6.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 4008 times.

This article's PDF has been downloaded 1055 times.