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 19 articles )

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

  1. Tomita, Takashi; Ueno, Atsushi; Shimakawa, Masaya; Hagihara, Shigeki; Yonezaki, Naoki: Safraless LTL synthesis considering maximal realizability (2017)
  2. Vasile, Cristian-Ioan; Aksaray, Derya; Belta, Calin: Time window temporal logic (2017)
  3. 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)
  4. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  5. Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István: Component-wise incremental LTL model checking (2016)
  6. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  7. Shan, Laixiang; Qin, Jun; Chen, Mingshi; Qin, Zheng: Degeneralization algorithm for generation of Büchi automata based on contented situation (2015)
  8. 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)
  9. Komárková, Zuzana; Křetínský, Jan: Rabinizer 3: safraless translation of LTL to small deterministic automata (2014)
  10. Duret-Lutz, Alexandre: Manipulating LTL formulas using Spot 1.0 (2013)
  11. Fronc, Łukasz; Duret-Lutz, Alexandre: LTL model checking with neco (2013)
  12. 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)
  13. Hallé, Sylvain; Villemaire, Roger; Cherkaoui, Omar; Deca, Rudy: A logical approach to data-aware automated sequence generation (2012)
  14. Tabakov, Deian; Rozier, Kristin Y.; Vardi, Moshe Y.: Optimized temporal monitors for SystemcC (2012)
  15. Rozier, Kristin Y.: Linear temporal logic symbolic model checking (2011)
  16. Rozier, Kristin Y.; Vardi, Moshe Y.: LTL satisfiability checking (2010) ioport
  17. Duret-Lutz, Alexandre; Poitrenaud, Denis; Couvreur, Jean-Michel: On-the-fly emptiness check of transition-based Streett automata (2009)
  18. Vardi, Moshe Y.: From philosophical to industrial logics (2009)
  19. Evangelista, Sami: High level Petri nets analysis with Helena (2005)