SPOT
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
Keywords for this software
References in zbMATH (referenced in 25 articles )
Showing results 1 to 20 of 25.
Sorted by year (- Blahoudek, František; Major, Juraj; Strejček, Jan: LTL to self-loop alternating automata with generic acceptance and back (2020)
- Baier, Christel; Blahoudek, František; Duret-Lutz, Alexandre; Klein, Joachim; Müller, David; Strejček, Jan: Generic emptiness check for fun and profit (2019)
- Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
- Löding, Christof; Pirogov, Anton: New optimizations and heuristics for determinization of Büchi automata (2019)
- Li, Jianwen; Zhang, Lijun; Zhu, Shufang; Pu, Geguang; Vardi, Moshe Y.; He, Jifeng: An explicit transition system construction approach to LTL satisfiability checking (2018)
- Tomita, Takashi; Ueno, Atsushi; Shimakawa, Masaya; Hagihara, Shigeki; Yonezaki, Naoki: Safraless LTL synthesis considering maximal realizability (2017)
- Vasile, Cristian-Ioan; Aksaray, Derya; Belta, Calin: Time window temporal logic (2017)
- 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)
- Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
- Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István: Component-wise incremental LTL model checking (2016)
- Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
- Shan, Laixiang; Du, Xiaomin; Qin, Zheng: Efficient approach of translating LTL formulae into Büchi automata (2015)
- Shan, Laixiang; Qin, Jun; Chen, Mingshi; Qin, Zheng: Degeneralization algorithm for generation of Büchi automata based on contented situation (2015)
- 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)
- Komárková, Zuzana; Křetínský, Jan: Rabinizer 3: Safraless translation of LTL to small deterministic automata (2014)
- Duret-Lutz, Alexandre: Manipulating LTL formulas using Spot 1.0 (2013)
- Fronc, Łukasz; Duret-Lutz, Alexandre: LTL model checking with Neco (2013)
- 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)
- Hallé, Sylvain; Villemaire, Roger; Cherkaoui, Omar; Deca, Rudy: A logical approach to data-aware automated sequence generation (2012)
- Tabakov, Deian; Rozier, Kristin Y.; Vardi, Moshe Y.: Optimized temporal monitors for SystemcC (2012)