 |
 |
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)2007From Nondeterministic Büchi and Streett Automata to Deterministic
Parity AutomataArticle
Authors: Nir Piterman 
0000-0002-8242-5357Nir 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).
Source: arXiv.org:0705.2205
Volume: Volume 3, Issue 3
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
Bibliographic References
98 Documents citing this article
- Michaël Cadilhac;Guillermo A. Pérez, Lecture Notes in Computer Science, Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability, pp. 192-207, 2023, 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;et al., 2023, Reasoning about Quality and Fuzziness of Strategic Behaviors, ACM Transactions on Computational Logic, 24, 3, pp. 1-38, 10.1145/3582498, https://doi.org/10.1145/3582498.
- Raven Beutner;Bernd Finkbeiner, Lecture Notes in Computer Science, AutoHyper: Explicit-State Model Checking for HyperLTL, pp. 145-163, 2023, 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, Lecture notes in computer science, Modular Mix-and-Match Complementation of Büchi Automata, pp. 249-270, 2023, 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 (Basel), 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., Lecture Notes in Computer Science, EPMC Gets Knowledge in Multi-agent Systems, pp. 93-107, 2022, 10.1007/978-3-030-94583-1_5.
- Daniel Hausmann;Nir Piterman, arXiv (Cornell University), A Survey on Satisfiability Checking for the $$\mu $$-Calculus Through Tree Automata, pp. 228-251, 2022, 10.1007/978-3-031-22337-2_11, https://arxiv.org/abs/2207.00517.
- 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 (Print), 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, Lecture notes in computer science, FORQ-Based Language Inclusion Formal Testing, pp. 109-129, 2022, 10.1007/978-3-031-13188-2_6, https://doi.org/10.1007/978-3-031-13188-2_6.
- Li, Yong;Turrini, Andrea;Feng, Weizhi;Vardi, Moshe Y.;Zhang, Lijun, Lecture notes in computer science, Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition, pp. 152-173, 2022, 10.1007/978-3-031-13188-2_8, https://doi.org/10.1007/978-3-031-13188-2_8.
- Vojtěch Havlena;Ondřej Lengál;Barbora Šmahlíková, Lecture notes in computer science, Sky Is Not the Limit, pp. 118-136, 2022, 10.1007/978-3-030-99527-0_7, https://doi.org/10.1007/978-3-030-99527-0_7.
- Vojtěch Havlena;Ondřej Lengál;Barbora Šmahlíková, Lecture notes in computer science, Complementing Büchi Automata with Ranker, pp. 188-201, 2022, 10.1007/978-3-031-13188-2_10, https://doi.org/10.1007/978-3-031-13188-2_10.
- Alessandro Abate;Julian Gutierrez;Lewis Hammond;Paul Harrenstein;Marta Kwiatkowska;et al., 2021, Rational verification: game-theoretic verification of multi-agent systems, Applied intelligence (Boston), 51, 9, pp. 6569-6584, 10.1007/s10489-021-02658-y, https://doi.org/10.1007/s10489-021-02658-y.
- Clemens Kupke;Johannes Marti;Yde Venema, 2021, On the size of disjunctive formulas in the μ-calculus, arXiv (Cornell University), 346, pp. 291-307, 10.4204/eptcs.346.19.
- Kyveli Doveri;Pierre Ganty;Francesco Parolini;Francesco Ranzato, Inclusion Testing of Büchi Automata Based on Well-Quasiorders, pp. 22-, 2021, 10.4230/lipics.concur.2021.3.
- León Bohn;Christof Löding, Constructing Deterministic ω-Automata from Examples by an Extension of the RPNI Algorithm., pp. 18-, 2021, 10.4230/lipics.mfcs.2021.20.
- 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, Lecture Notes in Computer Science, Linear Temporal Logic – From Infinite to Finite Horizon, pp. 3-12, 2021, 10.1007/978-3-030-88885-5_1.
- Stefan Kiefer;Pavel Semukhin;Cas Widdershoven, Linear-Time Model Checking Branching Processes, pp. 16-, 2021, 10.4230/lipics.concur.2021.6.
- Vojtěch Havlena;Ondřej Lengál;Barbora Šmahlíková, Lecture notes in computer science, Deciding S1S: Down the Rabbit Hole and Through the Looking Glass, pp. 215-222, 2021, 10.1007/978-3-030-91014-3_15.
- Cong Tian;Wensheng Wang;Zhenhua Duan, arXiv (Cornell University), Making Streett Determinization Tight, 2020, Saarbrücken Germany, 10.1145/3373718.3394757, http://arxiv.org/abs/2006.16476.
- Cristian S. Calude;Sanjay Jain;Bakhadyr Khoussainov;Wei Li;Frank Stephan, 2020, Deciding Parity Games in Quasi-polynomial Time, SIAM journal on computing (Print), 51, 2, pp. STOC17-188, 10.1137/17m1145288.
- Ernst Moritz Hahn;Mateo Perez;Sven Schewe;Fabio Somenzi;Ashutosh Trivedi;et al., Lecture Notes in Computer Science, Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning, pp. 306-323, 2020, 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, Lecture notes in computer science, Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization, pp. 15-27, 2020, 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 Association for Computing Machinery, 67, 6, pp. 1-61, 10.1145/3417995, https://doi.org/10.1145/3417995.
- Julian Gutierrez;Aniello Murano;Giuseppe Perelli;Sasha Rubin;Thomas Steeples;et al., 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 J. Wooldridge, 2020, Automated temporal equilibrium analysis: Verification and synthesis of multi-player games, Oxford University Research Archive (ORA) (University of Oxford), 287, pp. 103353, 10.1016/j.artint.2020.103353, https://ora.ox.ac.uk/objects/uuid:baf504e4-aabd-4939-bbe3-2023d7fe75c6.
- Christof Löding;Anton Pirogov, arXiv (Cornell University), New Optimizations and Heuristics for Determinization of Büchi Automata, pp. 317-333, 2019, 10.1007/978-3-030-31784-3_18, https://arxiv.org/abs/1911.01759.
- Jan Křetínský;Alexander Manta;Tobias Meggendorfer, arXiv (Cornell University), Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis, pp. 404-422, 2019, 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;et al., 2019, An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space, arXiv (Cornell University), 21, 3, pp. 325-349, 10.1007/s10009-019-00509-3, https://arxiv.org/abs/1703.01296.
- Udi Boker, Lecture Notes in Computer Science, Inherent Size Blowup in $$\omega $$ -Automata, pp. 3-17, 2019, 10.1007/978-3-030-24886-4_1.
- Yong Li;Andrea Turrini;Yu-Fang Chen;Lijun Zhang, Lecture Notes in Computer Science, Learning Büchi Automata and Its Applications, pp. 38-98, 2019, 10.1007/978-3-030-17601-3_2.
- Yong Li;Xuechao Sun;Andrea Turrini;Yu-Fang Chen;Junnan Xu, Lecture notes in computer science, ROLL 1.0: $$\omega $$ -Regular Language Learning Library, pp. 365-371, 2019, 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, Lecture notes in computer science, Simulations in Rank-Based Büchi Automata Complementation, pp. 447-467, 2019, 10.1007/978-3-030-34175-6_23.
- Daniel Hausmann;Lutz Schröder;Hans-Peter Deifel, Lecture notes in computer science, Permutation Games for the Weakly Aconjunctive $$\mu $$ μ -Calculus, pp. 361-378, 2018, 10.1007/978-3-319-89963-3_21, https://doi.org/10.1007/978-3-319-89963-3_21.
- Julian C. Bradfield;Igor Walukiewicz, The mu-calculus and Model Checking, pp. 871-919, 2018, 10.1007/978-3-319-10575-8_26, https://hal.archives-ouvertes.fr/hal-02397703.
- Orna Kupferman, Springer eBooks, Automata Theory and Model Checking, pp. 107-151, 2018, 10.1007/978-3-319-10575-8_4.
- Ayrat Khalimov;Roderick Bloem, Lecture Notes in Computer Science, Bounded Synthesis for Streett, Rabin, and $$\text {CTL}^{*}$$, pp. 333-352, 2017, 10.1007/978-3-319-63390-9_18.
- Bérard, Béatrice;Kouchnarenko, Olga;Mullins, John;Sassolas, Mathieu, 2017, Opacity for linear constraint Markov chains, Discrete event dynamic systems, 28, 1, pp. 83-108, 10.1007/s10626-017-0259-4, https://hal.sorbonne-universite.fr/hal-01384153/file/bkms-hal.pdf.
- Cristian S. Calude;Sanjay Jain;Bakhadyr Khoussainov;Wei Li;Frank Stephan, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, Deciding parity games in quasipolynomial time, 2017, Montreal Canada, 10.1145/3055399.3055409.
- Jan Křetínský;Tobias Meggendorfer;Clara Waldmann;Maximilian Weininger, arXiv (Cornell University), Index Appearance Record for Transforming Rabin Automata into Parity Automata, pp. 443-460, 2017, 10.1007/978-3-662-54577-5_26, https://arxiv.org/abs/1701.05738.
- Javier Esparza;Jan Křetínský;Jean-François Raskin;Salomon Sickert, arXiv (Cornell University), From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata, pp. 426-442, 2017, 10.1007/978-3-662-54577-5_25, https://arxiv.org/abs/1701.06103.
- Krishnendu Chatterjee;Laurent Doyen;Emmanuel Filiot;Jean-François Raskin, 2017, Doomsday equilibria for omega-regular games, CiteSeer X (The Pennsylvania State University), 254, pp. 296-315, 10.1016/j.ic.2016.10.012, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.724.2088.
- Orna Kupferman;Gal Vardi, 2017, On relative and probabilistic finite counterability, Leibniz-Zentrum für Informatik (Schloss Dagstuhl), 52, 2, pp. 117-146, 10.1007/s10703-017-0277-8, https://drops.dagstuhl.de/opus/volltexte/2015/5414/.
- Paul William Hunter;Guillermo A. Perez;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.
- Sven Schewe, 2017, Solving parity games in big steps, Journal of computer and system sciences (Print), 84, pp. 243-262, 10.1016/j.jcss.2016.10.002, https://doi.org/10.1016/j.jcss.2016.10.002.
- 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, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, Towards Completeness via Proof Search in the Linear Time μ-calculus, 2016, New York NY USA, 10.1145/2933575.2933598.
- Beatrice Berard;Olga Kouchnarenko;John Mullins;Mathieu Sassolas, Preserving opacity on Interval Markov Chains under simulation, 2016, Xi'an, China, 10.1109/wodes.2016.7497866.
- Bernd Finkbeiner;Felix Klein, Lecture notes in computer science, Bounded Cycle Synthesis, pp. 118-135, 2016, 10.1007/978-3-319-41528-4_7.
- Dana Fisman, Lecture notes in computer science, A Complexity Measure on Büchi Automata, pp. 102-113, 2016, 10.1007/978-3-319-30000-9_8.
- František Blahoudek;Matthias Heizmann;Sven Schewe;Jan Strejček;Ming-Hsien Tsai, Lecture Notes in Computer Science, Complementing Semi-deterministic Büchi Automata, pp. 770-787, 2016, 10.1007/978-3-662-49674-9_49.
- 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 IEEE 55th Conference on Decision and Control (CDC), Risk-averse control of Markov decision processes with ω-regular objectives, 2016, Las Vegas, NV, USA, 10.1109/cdc.2016.7798306.
- Salomon Sickert;Javier Esparza;Stefan Jaax;Jan Křetínský, Lecture notes in computer science, Limit-Deterministic Büchi Automata for Linear Temporal Logic, pp. 312-332, 2016, 10.1007/978-3-319-41540-6_17.
- Souymodip Chakraborty;Joost-Pieter Katoen, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, On the Satisfiability of Some Simple Probabilistic Logics, 2016, New York NY USA, 10.1145/2933575.2934526.
- Christian 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/record/283987/files/Essen-Jobstmann2015_Article_ProgramRepairWithoutRegret.pdf.
- 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., Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Temporal logic motion planning using POMDPs with parity objectives, 2015, Seattle Washington, 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 William Hunter;Guillermo G.A. Pérez;Jean-François Raskin, Institutional Repository University of Antwerp (University of Antwerp), Looking at Mean-Payoff Through Foggy Windows, pp. 429-445, 2015, 10.1007/978-3-319-24953-7_31, https://repository.uantwerpen.be/docman/irua/a02de3/154951.pdf.
- Rachel Faran;Orna Kupferman, Lecture notes in computer science, Spanning the Spectrum from Safety to Liveness, pp. 183-200, 2015, 10.1007/978-3-319-24953-7_13.
- Steen Vester, Technical University of Denmark, DTU Orbit (Technical University of Denmark, DTU), On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems, pp. 361-377, 2015, 10.1007/978-3-319-24953-7_27, https://backend.orbit.dtu.dk/ws/files/118019604/main.pdf.
- Sven Schewe;Ashutosh Trivedi;Thomas Varghese, arXiv (Cornell University), Symmetric Strategy Improvement, pp. 388-400, 2015, 10.1007/978-3-662-47666-6_31, https://arxiv.org/abs/1501.06484.
- 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, CiteSeer X (The Pennsylvania State University), Doomsday Equilibria for Omega-Regular Games, pp. 78-97, 2014, 10.1007/978-3-642-54013-4_5, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.590.8912.
- Shaull Almagor;Orna Kupferman, Lecture Notes in Computer Science, Latticed-LTL Synthesis in the Presence of Noisy Inputs, pp. 226-241, 2014, 10.1007/978-3-642-54830-7_15, https://doi.org/10.1007/978-3-642-54830-7_15.
- Sven Schewe;Thomas Varghese, arXiv (Cornell University), Determinising Parity Automata, pp. 486-498, 2014, 10.1007/978-3-662-44522-8_41, https://arxiv.org/abs/1401.5394.
- Sven Schewe;Thomas Varghese, arXiv (Cornell University), Tight Bounds for Complementing Parity Automata, pp. 499-510, 2014, 10.1007/978-3-662-44522-8_42, https://arxiv.org/abs/1406.1090.
- Zuzana Komárková;Jan Křetínský, Lecture notes in computer science, Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata, pp. 235-241, 2014, 10.1007/978-3-319-11936-6_17.
- Christian von Essen;Barbara Jobstmann, Lecture Notes in Computer Science, Program Repair without Regret, pp. 896-911, 2013, 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, Lecture notes in computer science, Deternimization of Büchi Automata as Partitioned Automata, pp. 158-168, 2013, 10.1007/978-3-642-38768-5_16.
- František Blahoudek;Mojmír Křetínský;Jan Strejček, Lecture notes in computer science, Comparison of LTL to Deterministic Rabin Automata Translators, pp. 164-172, 2013, 10.1007/978-3-642-45221-5_12.
- Krishnendu Chatterjee;Andreas Gaiser;Jan Křetínský, Lecture notes in computer science, Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis, pp. 559-575, 2013, 10.1007/978-3-642-39799-8_37, https://doi.org/10.1007/978-3-642-39799-8_37.
- Nir Piterman, Lecture Notes in Computer Science, Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development, pp. 45-49, 2013, 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 (Print), 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, arXiv (Cornell University), 119, pp. 107-121, 10.4204/eptcs.119.11.
- Tomáš Babiak;František Blahoudek;Mojmír Křetínský;Jan Strejček, arXiv (Cornell University), Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment, pp. 24-39, 2013, 10.1007/978-3-319-02444-8_4.
- Jan Křetínský;Javier Esparza, Lecture notes in computer science, Deterministic Automata for the (F,G)-Fragment of LTL, pp. 7-22, 2012, 10.1007/978-3-642-31424-7_7, https://doi.org/10.1007/978-3-642-31424-7_7.
- Orna Kupferman, Lecture notes in computer science, Recent Challenges and Ideas in Temporal Synthesis, pp. 88-98, 2012, 10.1007/978-3-642-27660-6_8.
- Orna Kupferman;Dorsa Sadigh;Sanjit A. Seshia, CiteSeer X (The Pennsylvania State University), Synthesis with Clairvoyance, pp. 5-19, 2012, 10.1007/978-3-642-34188-5_5, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.305.1272.
- 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, Lecture Notes in Computer Science, Improved Ramsey-Based Büchi Complementation, pp. 150-164, 2012, 10.1007/978-3-642-28729-9_10, https://doi.org/10.1007/978-3-642-28729-9_10.
- Sven Schewe;Thomas Varghese, Lecture notes in computer science, Tight Bounds for the Determinisation and Complementation of Generalised Büchi Automata, pp. 42-56, 2012, 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, arXiv (Cornell University), 54, pp. 178-191, 10.4204/eptcs.54.13.
- Barbara Di Giampaolo;Gilles Geeraerts;Jean-François Raskin;Nathalie Sznajder, CiteSeer X (The Pennsylvania State University), Safraless Procedures for Timed Specifications, pp. 2-22, 2010, 10.1007/978-3-642-15297-9_2, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.3704.
- Orna Kupferman;Moshe Y. Vardi, CiteSeer X (The Pennsylvania State University), Synthesis of Trigger Properties, pp. 312-331, 2010, 10.1007/978-3-642-17511-4_18, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.300.1821.
- Patrice Godefroid;Nir Piterman, 2010, LTL generalized model checking revisited, INDIGO (University of Illinois at Chicago), 13, 6, pp. 571-584, 10.1007/s10009-010-0169-3, https://figshare.com/articles/journal_contribution/LTL_generalized_model_checking_revisited/10105835.
- Emmanuel Filiot;Naiyong Jin;Jean-François Raskin, Lecture Notes in Computer Science, An Antichain Algorithm for LTL Realizability, pp. 263-277, 2009, 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, Lecture Notes in Computer Science, Realizability of Real-Time Logics, pp. 133-148, 2009, 10.1007/978-3-642-04368-0_12.
- Sven Schewe, Lecture Notes in Computer Science, From Parity and Payoff Games to Linear Programming, pp. 675-686, 2009, 10.1007/978-3-642-03816-7_57.
- Sven Schewe, Lecture Notes in Computer Science, Tighter Bounds for the Determinisation of Büchi Automata, pp. 167-181, 2009, 10.1007/978-3-642-00596-1_13, https://doi.org/10.1007/978-3-642-00596-1_13.
- Thomas Colcombet;Konrad Zdanowski, Lecture notes in computer science, A Tight Lower Bound for Determinization of Transition Labeled Büchi Automata, pp. 151-162, 2009, 10.1007/978-3-642-02930-1_13.
- Karin Greimel;Roderick Bloem;Barbara Jobstmann;Moshe Vardi, Lecture Notes in Computer Science, Open Implication, pp. 361-372, 2008, 10.1007/978-3-540-70583-3_30.
- Patrice Godefroid;Nir Piterman, INDIGO (University of Illinois at Chicago), LTL Generalized Model Checking Revisited, pp. 89-104, 2008, 10.1007/978-3-540-93900-9_11, https://figshare.com/articles/journal_contribution/LTL_generalized_model_checking_revisited/10105835.
- Orna Kupferman;Nir Piterman;Moshe Y. Vardi, Lecture Notes in Computer Science, Safraless Compositional Synthesis, pp. 31-44, 2006, 10.1007/11817963_6, https://doi.org/10.1007/11817963_6.
Share and export
Consultation statistics
This page has been seen 1389 times.
This article's PDF has been downloaded 604 times.