spot  2.11.6
Bibliography
[1]

Tomás Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Kretínsky, and Jan Strejcek. Compositional approach to suspension and other improvements to LTL translation. In Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN'13), volume 7976 of Lecture Notes in Computer Science, pages 81–98. Springer, July 2013.

[2]

Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, and Jan Strejcek. Generic emptiness check for fun and profit. In Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA'19), volume 11781 of Lecture Notes in Computer Science, pages 445–461. Springer, October 2019.

[3]

Michael Benedikt, Rastislav Lenhardt, and James Worrell. LTL model checking of interval markov chains. In Nir Piterman and Scott A. Smolka, editors, 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of Lecture Notes in Computer Science, pages 32–46. Springer, 2013.

[4]

Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, and Ming-Hsien Tsai. Complementing semi-deterministic Büchi automata. In Marsha Chechik and Jean-François Raskin, editors, Proceedings of the 22th International Conférence on Tools and Algorithms for the Construction and Analysis of Systems, pages 770–787. Springer, 2016.

[5]

Udi Boker and Orna Kupferman. Co-büching them all. pages 184–198, 2011.

[6]

Anne Brüggemann-Klein. Regular expressions into finite automata. Theoretical Computer Science, 120:87–98, 1996.

[7]

Olivier Carton and Ramón Maceiras. Computing the Rabin index of a parity automaton. Informatique théorique et applications, 33(6):495–505, 1999.

[8]

Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal transformations of games and automata using Muller conditions. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, Proceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP'21), volume 198 of Leibniz International Proceedings in Informatics (LIPIcs), pages 123:1–123:14, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[9]

Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, and Salomon Sickert. Practical applications of the Alternating Cycle Decomposition. In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 13244 of Lecture Notes in Computer Science, pages 99–117, April 2022.

[10]

Jacek Cichon, Adam Czubak, and Andrzej Jasinski. Minimal Büchi automata for certain classes of LTL formulas. In Proceedings of the Fourth International Conference on Dependability of Computer Systems, pages 17–24. IEEE Computer Society, 2009.

[11]

Alessandro Cimatti, Marco Roveri, Simone Semprini, and Stefano Tonetta. From PSL to NBA: a modular symbolic encoding. In Proceedings of the 6th conference on Formal Methods in Computer Aided Design (FMCAD'06), pages 125–133. IEEE Computer Society, 2006.

[12]

Lorenzo Clemente and Richard Mayr. Efficient reduction of nondeterministic automata with application to language inclusion testing. CoRR, abs/1711.09946, 2017.

[13]

Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, and Mihalis Yannakakis. Memory-efficient algorithm for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.

[14]

Jean-Michel Couvreur. On-the-fly verification of temporal logic. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99), volume 1708 of Lecture Notes in Computer Science, pages 253–271. Springer-Verlag, September 1999.

[15]

Christian Dax, Jochen Eisinger, and Felix Klaedtke. Mechanizing the powerset construction for restricted classes of ω-automata. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), volume 4762 of Lecture Notes in Computer Science. Springer-Verlag, October 2007.

[16]

Christian Dax, Felix Klaedtke, and Stefan Leue. Specification languages for stutter-invariant regular properties. In Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), volume 5799 of Lecture Notes in Computer Science, pages 244–254. Springer-Verlag, 2009.

[17]

Alexandre Duret-Lutz. LTL translation improvements in Spot 1.0. International Journal on Critical Computer-Based Systems, 5(1/2):31–54, March 2014.

[18]

Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Property specification patterns for finite-state verification. In Mark Ardis, editor, Proceedings of the 2nd Workshop on Formal Methods in Software Practice (FMSP'98), pages 7–15. ACM Press, March 1998.

[19]

Kousha Etessami and Gerard J. Holzmann. Optimizing Büchi automata. In C. Palamidessi, editor, Proceedings of the 11th International Conference on Concurrency Theory (Concur'00), volume 1877 of Lecture Notes in Computer Science, pages 153–167, Pennsylvania, USA, 2000. Springer-Verlag. Beware of a typo in the version from the proceedings: f U g is purely eventual if both operands are purely eventual. The revision of the paper available at http://www.bell-labs.com/project/TMP/ is fixed. We fixed the bug in Spot in 2005, thanks to LBTT. See also http://arxiv.org/abs/1011.4214v2 for a discussion about this problem.

[20]

Kousha Etessami. A note on a question of Peled and Wilke regarding stutter-invariant LTL. Information Processing Letters, 75(6):261–263, 2000.

[21]

Bernd Finkbeiner, Gideon Geier, and Noemi Passing. Specification decomposition for reactive synthesis. In Procedings of NASA Formal Methods (NFM'21), volume 12673 of Lecture Notes in Computer Science. Springer, 2021.

[22]

Bernd Finkbeiner, Gideon Geier, and Noemi Passing. Specification decomposition for reactive synthesis (full version). Technical report, 2021.

[23]

Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01), volume 2102 of Lecture Notes in Computer Science, pages 53–65. Springer-Verlag,

[24]

Jaco Geldenhuys and Henri Hansen. Larger automata and less work for LTL model checking. In Proceedings of the 13th International SPIN Workshop (SPIN'06), volume 3925 of Lecture Notes in Computer Science, pages 53–70. Springer, 2006.

[25]

Jaco Geldenhuys and Antti Valmari. Tarjan's algorithm makes on-the-fly LTL verification more efficient. In Kurt Jensen and Andreas Podelski, editors, Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 205–219. Springer-Verlag,

[26]

Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Francesca Rossi, editor, Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI'13), pages 854–860, August 2013.

[27]

J. Holecek, T. Kratochvíla, V. Rehák, D. Safránek, and P. Simecek. Verification results in Liberouter project. Technical Report 03, CESNET, September 2004.

[28]

Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs, New Jersey, 1991.

[29]

Shin ichi Minato. Fast generation of irredundant sum-of-products forms from binary decision diagrams. In Proceedings of the third Synthesis and Simulation and Meeting International Interchange workshop (SASIMI'92), pages 64–73, Kobe, Japan, April 1992.

[30]

Swen Jacobs, Felix Klein, and Sebastian Schirmer. A high-level LTL synthesis format: TLSF v1.1. In Proceedings Fifth Workshop on Synthesis (SYNT@CAV'16), volume 229 of Electronic Proceedings in Theoretical Computer Science, pages 112–132, 2016.

[31]

Joachim Klein and Christel Baier. On-the-fly stuttering in the construction of deterministic ω-automata. In Jan Holub and Jan Žďárek, editors, Proceedings of the 12th International Conference on the Implementation and Application of Automata (CIAA'07), volume 4783 of Lecture Notes in Computer Science, pages 51–61. Springer, 2007.

[32]

Orna Kupferman and Adin Rosenberg. The blow-up in translating LTL do deterministic automata. In Proceedings of the 6th International Workshop on Model Checking and Artificial Intelligence (MoChArt 2010), volume 6572 of Lecture Notes in Artificial Intelligence, pages 85–94. Springer, November 2011. See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf.

[33]

Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic (TOCL), 2(3):408–429, July

[34]

Orna Kupferman and Moshe Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273–294, April 2005.

[35]

Orna Kupferman and Moshe Y. Vardi. From complementation to certification. Theoretical Computer Science, 345(1):83–100, November 2005.

[36]

Jan Kretínsky, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger. Index appearance record for transforming Rabin automata into parity automata. In Axel Legay and Tiziana Margaria, editors, Proceedings of the 23st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), volume 10205 of Lecture Notes in Computer Science, pages 443–460, 2017.

[37]

George Loizou and Peter Thanisch. Enumerating the cycles of a digraph: A new preprocessing strategy. Information Sciences, 27(3):163–182, August 1982.

[38]

Christof Löding. Methods for the transformation of ω-automata: Complexity and connection to second order logic. Master's thesis, Institute of Computer Science and Applied Mathematics Christian-Albrechts-University of Kiel, 1998.

[39]

Thibaud Michaud and Alexandre Duret-Lutz. Practical stutter-invariance checks for ω-regular languages. In Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15), volume 9232 of Lecture Notes in Computer Science, pages 84–101. Springer, August 2015.

[40]

David Müller and Salomon Sickert. LTL to deterministic Emerson-Lei automata. In Proceedings of the 8th International Sumposium on Games, Automata, Logics and Formal Verification (GandALF'17), volume 256 of Electronic Proceedings in Theoretical Computer Science, pages 180–194. Open Publishing Association, 2017.

[41]

Radek Pelánek. BEEM: benchmarks for explicit model checkers. In Proceedings of the 14th international SPIN conference on Model checking software, volume 4595 of Lecture Notes in Computer Science, pages 263–267. Springer-Verlag, 2007.

[42]

Guillermo A. Pérez. The extended HOA format for synthesis. ArXiv, dec 2019.

[43]

Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. In E. Allen Emerson and Kedar S. Namjoshi", editors, Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'06), volume 3855 of Lecture Notes in Computer Science, pages 364–380. Springer, 2006.

[44]

Roman Redziejowski. An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae, 119(3-4):393–406, 2012.

[45]

Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud. Strength-based decomposition of the property Büchi automaton for faster model checking. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of Lecture Notes in Computer Science, pages 580–593. Springer, 2013.

[46]

Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, and Adrien Pommellet. Effective reductions of Mealy machines. In Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'22), volume 13273 of Lecture Notes in Computer Science, pages 170–187. Springer, June 2022.

[47]

Kristin Y. Rozier and Moshe Y. Vardi. Ltl satisfiability checking. In Proceedings of the 12th International SPIN Workshop on Model Checking of Software (SPIN'07), volume 4595 of Lecture Notes in Computer Science, pages 149–167. Springer-Verlag, 2007.

[48]

Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. Technical Report 2004/06, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, November 2004.

[49]

Roberto Sebastiani and Stefano Tonetta. "more deterministic" vs. "smaller" büchi automata for efficient ltl model checking. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Proceedings for the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), volume 2860 of Lectures Notes in Computer Science, pages 126–140. Springer-Verlag, October 2003.

[50]

Salomon Sickert, Javier Esparza, Stefaan Jaax, and Jan Kretínsky. Limit-deterministic Büchi automata for linear temporal logic. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV'16), volume 9780 of Lecture Notes in Computer Science, pages 312–332. Springer-Verlag, 2016.

[51]

Fabio Somenzi and Roderick Bloem. Efficient Büchi automata for LTL formulae. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00), volume 1855 of Lecture Notes in Computer Science, pages 247–263, Chicago, Illinois, USA, 2000. Springer-Verlag.

[52]

Deian Tabakov and Moshe Y. Vardi. Optimized temporal monitors for SystemC. In Proceedings of the 1st International Conference on Runtime Verification (RV'10), volume 6418 of Lecture Notes in Computer Science, pages 436–451. Springer, November 2010.

[53]

Heikki Tauriainen. Automated testing of Büchi automata translators for Linear Temporal Logic. Research Report A66, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2000. Reprint of Master's thesis.

[54]

Heikki Tauriainen. On translating linear temporal logic into alternating and nondeterministic automata. Research Report A83, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2003. Reprint of Licentiate's thesis.

[55]

Heikki Tauriainen. Automata and linear temporal logic: Translations with transition-based acceptance. Research Report A104, Espoo, Finland, September 2006. Doctoral dissertation.

[56]

Xavier Thirioux. Simple and efficient translation from LTL formulas to Büchi automata. In Rance Cleaveland and Hubert Garavel, editors, Proceedings of the 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems (FMICS'02), volume 66(2) of Electronic Notes in Theoretical Computer Science, Málaga, Spain, July 2002. Elsevier.

[57]

Tom van Dijk. Oink: An implementation and evaluation of modern parity game solvers. In Dirk Beyer and Marieke Huisman, editors, Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), volume 10805 of Lecture Notes in Computer Science, pages 291–308. Springer, 2018.

[58]

Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1):135–183, 1998.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1