SPOT: an extensible model checking library using transition-based generalized Büchi automata. SPOT (SPOT produces our traces), is a C++ library offering model checking bricks that can be combined and interfaced with third party tools to build a model checker. It relies on transition-based generalized Büchi automata (TGBA) and does not need to degeneralize these automata to check their emptiness. We motivate the choice of TGBA by illustrating a very simple (yet efficient) translation of LTL (linear temporal logic) into TGBA. We then show how it supports on-the-fly computations, and how it can be extended or integrated in other tools

References in zbMATH (referenced in 25 articles )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Blahoudek, František; Major, Juraj; Strejček, Jan: LTL to self-loop alternating automata with generic acceptance and back (2020)
  2. Baier, Christel; Blahoudek, František; Duret-Lutz, Alexandre; Klein, Joachim; Müller, David; Strejček, Jan: Generic emptiness check for fun and profit (2019)
  3. Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
  4. Löding, Christof; Pirogov, Anton: New optimizations and heuristics for determinization of Büchi automata (2019)
  5. Li, Jianwen; Zhang, Lijun; Zhu, Shufang; Pu, Geguang; Vardi, Moshe Y.; He, Jifeng: An explicit transition system construction approach to LTL satisfiability checking (2018)
  6. Tomita, Takashi; Ueno, Atsushi; Shimakawa, Masaya; Hagihara, Shigeki; Yonezaki, Naoki: Safraless LTL synthesis considering maximal realizability (2017)
  7. Vasile, Cristian-Ioan; Aksaray, Derya; Belta, Calin: Time window temporal logic (2017)
  8. Chivilikhin, D. S.; Ulyantsev, V. I.; Shalyto, A. A.: Modified ant colony algorithm for constructing finite state machines from execution scenarios and temporal formulas (2016)
  9. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  10. Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István: Component-wise incremental LTL model checking (2016)
  11. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  12. Shan, Laixiang; Du, Xiaomin; Qin, Zheng: Efficient approach of translating LTL formulae into Büchi automata (2015)
  13. Shan, Laixiang; Qin, Jun; Chen, Mingshi; Qin, Zheng: Degeneralization algorithm for generation of Büchi automata based on contented situation (2015)
  14. Taha, Safouan; Julliand, Jacques; Dadeau, Frédéric; Castillos, Kalou Cabrera; Kanso, Bilal: A compositional automata-based semantics and preserving transformation rules for testing property patterns (2015)
  15. Komárková, Zuzana; Křetínský, Jan: Rabinizer 3: Safraless translation of LTL to small deterministic automata (2014)
  16. Duret-Lutz, Alexandre: Manipulating LTL formulas using Spot 1.0 (2013)
  17. Fronc, Łukasz; Duret-Lutz, Alexandre: LTL model checking with Neco (2013)
  18. Li, Jianwen; Pu, Geguang; Zhang, Lijun; Wang, Zheng; He, Jifeng; Guldstrand Larsen, Kim: On the relationship between LTL normal forms and Büchi automata (2013)
  19. Hallé, Sylvain; Villemaire, Roger; Cherkaoui, Omar; Deca, Rudy: A logical approach to data-aware automated sequence generation (2012)
  20. Tabakov, Deian; Rozier, Kristin Y.; Vardi, Moshe Y.: Optimized temporal monitors for SystemcC (2012)

1 2 next