• PRISM

  • Referenced in 289 articles [sw01186]
  • against specifications written in the probabilistic temporal logics PCTL and CSL. The tool features three...
  • Kronos

  • Referenced in 253 articles [sw01270]
  • expressed in the real-time temporal logic TCTL...
  • CESAR

  • Referenced in 114 articles [sw08510]
  • formulas of a branching time logic, the temporal operators of which can be computed iteratively...
  • BIOCHAM

  • Referenced in 37 articles [sw09927]
  • inferring unknown model parameters from temporal logic constraints. Biocham is mainly composed of : a rule ... several simulators (boolean, differential, stochastic), a temporal logic based language to formalize the temporal properties ... kinetic parameters in high dimension from temporal logic constraints. Biocham is a free software protected...
  • METATEM

  • Referenced in 54 articles [sw06568]
  • methodology for the use of temporal logic as an executable imperative language is introduced ... concrete framework, called METATEM, for executing temporal formulae, is motivated and illustrated through examples ... relating to the METATEM approach to executable logics...
  • Cadence SMV

  • Referenced in 26 articles [sw07795]
  • that allows you to formally verify temporal logic properties of finite state systems, such...
  • BPEL2oWFN

  • Referenced in 25 articles [sw06956]
  • Petri net property, or check any temporal logic formula with a variety of model checking...
  • MCMAS

  • Referenced in 24 articles [sw09463]
  • Verification of Multi-Agent Systems. While temporal logic in its various forms has proven essential...
  • TLA

  • Referenced in 23 articles [sw04442]
  • stands for the Temporal Logic of Actions, but it has become a shorthand for referring...
  • SCR

  • Referenced in 20 articles [sw06939]
  • succ. This slight extension of first-order logic allows us to increase the readability ... simple and avoids the complexity of temporal logic...
  • CACTUS

  • Referenced in 14 articles [sw02907]
  • Cactus has been proposed as a temporal logic programming language based on the branching notion ... time. Cactus supports two main operators: the temporal operator first which refers to the first...
  • JPAX

  • Referenced in 8 articles [sw09906]
  • user provided properties formulated in temporal logic. JPAX can in addition analyze the program ... specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race ... analysis. Temporal logic specifications can be formulated by the user in the Maude rewriting logic ... logic, but here extended with executable temporal logic. The Maude rewriting engine is then activated...
  • PGSolver

  • Referenced in 14 articles [sw14051]
  • well as model checking) for temporal logics. In this paper we investigate practical aspects...
  • TLPVS

  • Referenced in 9 articles [sw10024]
  • implementation of a linear temporal logic verification system. The system includes a set of theories ... defining a temporal logic, a number of proof rules for proving soundness and response properties...
  • TRP++

  • Referenced in 8 articles [sw14679]
  • theorem prover for Propositional Linear Time Temporal Logic based on the temporal resolution calculus ... clausal resolution approach to propositional temporal logic; Creating an experimental environment to try different modifications...
  • PVeStA

  • Referenced in 12 articles [sw08423]
  • PCTL/CSL, or (ii) the QuaTEx quantitative temporal logic. As our experiments show, the performance gains...
  • SCTL-MUS

  • Referenced in 8 articles [sw02245]
  • this model, a multi-valued causal temporal logic, referred to as Simple Causal Temporal Logic...
  • TTM

  • Referenced in 8 articles [sw11997]
  • Tableau-based Theorem Prover for Temporal Logic PLTL. TTM is a theorem prover ... Propositional Linear Temporal Logic called PLTL. TTM allows you to test the satisfiability...
  • TeMP

  • Referenced in 9 articles [sw09989]
  • temporal monodic prover. First-Order Temporal Logic, FOTL, is an extension of classical first-order ... logic by temporal operators for a discrete linear model of time (isomorphic to ℕ, that ... used model of time). Formulae of this logic are interpreted over structures that associate with...
  • SPOT

  • Referenced in 11 articles [sw09473]
  • efficient) translation of LTL (linear temporal logic) into TGBA. We then show how it supports...