• SAL

  • Referenced in 9 articles [sw13318]
  • three different high-performance model checkers for LTL: symbolic, bounded, and infinite-bounded. The infinite...
  • Helena

  • Referenced in 6 articles [sw33425]
  • specifications into Promela and check satisfaction of LTL properties with Spin [11]. To prove ... Promela translation satisfy the same LTL formulae (without next). Our correctness proof relies...
  • iscasMc

  • Referenced in 8 articles [sw36939]
  • particularly efficient in evaluating the probabilities of LTL properties...
  • ltl2dstar

  • Referenced in 4 articles [sw21007]
  • ltl2dstar (”LTL to deterministic Streett and Rabin automata”) is a program that converts formulas ... smaller automata in practice. It uses external LTL-to-Büchi translators for the conversion from ... LTL to NBA and can thus benefit from the state-of-the-art algorithms, implementations...
  • AdamMC

  • Referenced in 3 articles [sw34180]
  • Petri nets with transits and flow-LTL. The correctness of networks is often described ... with transits extend Petri nets and Flow-LTL extends LTL such that the data flows ... Petri nets with transits against Flow-LTL. We describe how AdamMC can automatically encode concurrent ... network specifications can be expressed in Flow-LTL. Underlying AdamMC is a reduction...
  • Z2sal

  • Referenced in 6 articles [sw07087]
  • four model checkers including those for LTL and CTL. The translation scheme preserves...
  • FaPAS

  • Referenced in 4 articles [sw10957]
  • affine (PWA) systems from linear temporal logic (LTL) specifications. Specifically, given a PWA system ... LTL specification, both tools search for the largest region of initial conditions, from which...
  • HyComp

  • Referenced in 4 articles [sw20163]
  • dynamics. HyComp can verify invariant and LTL properties, and scenario specifications; it can also perform ... case of scenario or LTL verification, or applying off-the-shelf algorithms based...
  • BioModelAnalyzer

  • Referenced in 3 articles [sw23594]
  • Bringing LTL model checking to biologists. The BioModelAnalyzer (BMA) is a web based tool ... perform simulations. Here we describe the LTL module, which includes a graphical and natural language ... interfaces to testing LTL queries. The graphical interface allows for graphical construction of the queries...
  • Charlie

  • Referenced in 4 articles [sw12881]
  • Petri nets, complemented by explicit CTL and LTL model checking. Charlie comes with a plugin...
  • RiTHM

  • Referenced in 4 articles [sw16439]
  • program under inspection and a set of LTL properties as input and generates an instrumented...
  • LTLAutomizer

  • Referenced in 2 articles [sw23307]
  • Ultimate LTLAutomizer: Ultimate LTL Automizer uses Büchi programs to prove that a C program satisfies ... LTL property. Ultimate LTL Automizer is a toolchain of the Ultimate software analysis framework...
  • kPWorkbench

  • Referenced in 3 articles [sw19654]
  • framework supports both Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) properties by making...
  • ITS-Tools

  • Referenced in 3 articles [sw29142]
  • diagrams (SDD) that supports reachability, CTL and LTL model-checking and a user-friendly eclipse...
  • J-LO

  • Referenced in 3 articles [sw32260]
  • specified using a linear time logic (LTL) over AspectJ pointcuts. Specification takes place right...
  • LTL_to_GBA

  • Referenced in 1 article [sw29245]
  • LTL_to_GBA: Converting Linear-Time Temporal Logic to Generalized Büchi Automata. We formalize linear ... time temporal logic (LTL) and the algorithm by Gerth et al. to convert LTL formulas ... that can be applied to optimize the LTL formula before conversion. Moreover, we integrate ... Merz, adapting the lemma that next-free LTL formula cannot distinguish between stuttering equivalent runs...
  • ltl3tela

  • Referenced in 1 article [sw37532]
  • LTL to self-loop alternating automata with generic acceptance and back. Self-loop alternating automata ... intermediate results in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA ... Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly ... translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations...
  • neco-spot

  • Referenced in 1 article [sw09474]
  • LTL model checking with neco. We introduce neco-spot, an LTL model checker for Petri ... combined with Spot to build an LTL model checker...
  • conPAS

  • Referenced in 1 article [sw10953]
  • from specifications given as Linear Temporal Logic (LTL) formulas. conPAS consists of two main steps ... techniques from Buchi games and qualitative probabilistic LTL model checking, it generates a control strategy ... while its extension conPAS2 can handle arbitrary LTL formulas through a translation to deterministic Rabin...
  • BeepBeep

  • Referenced in 2 articles [sw02026]
  • expressed internally in an extension of LTL with first-order quantification; they can be transparently...