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

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

1 2 next

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

1 2 next