• UMDES

  • Referenced in 359 articles [sw09523]
  • discrete event systems modeled by finite-state automata (FSA). There are routines for the manipulation...
  • HyTech

  • Referenced in 327 articles [sw04125]
  • Hybrid systems are specified as collections of automata with discrete and continuous components, and temporal...
  • Kronos

  • Referenced in 263 articles [sw01270]
  • real-time systems are modeled by timed automata and the correctness requirements are expressed...
  • MONA

  • Referenced in 122 articles [sw06170]
  • years, including formula reductions, DAGification, guided tree automata, three-valued logic, eager minimization, BDD-based ... automata representations, and cache-conscious data structures. We describe these techniques and quantify their respective...
  • Esterel

  • Referenced in 163 articles [sw20012]
  • systems, including real-time systems and control automata. The Esterel v5 compiler can be used...
  • LTL2BA

  • Referenced in 99 articles [sw10956]
  • Fast LTL to Büchi automata translation. We present an algorithm to generate Büchi automata from...
  • Timbuk

  • Referenced in 46 articles [sw06351]
  • Term Rewriting Systems and for manipulating Tree Automata (bottom-up non-deterministic finite tree automata ... fully new version of the tree automata completion engine used for reachability analysis. Older Timbuk ... Caml functions for basic manipulation on Tree Automata, alphabets, terms, Term Rewriting Systems...
  • TREX

  • Referenced in 46 articles [sw01388]
  • tool for automatic analysis of automata-based models equipped with variables belonging to different infinite/finite ... present time, parametric (continuous-time) timed automata, extended with integer counters and finite-domain variables...
  • VerICS

  • Referenced in 33 articles [sw02011]
  • original tool for automated verification of Timed Automata and protocols written in a subset ... original intermediate language (IL), or Timed Automata in the Kronos-like format can be used ... specification can be translated to timed automata, which are passed to other Verics components ... translating the reachability problem for Timed Automata to the satisfiability problem of propositional formulas...
  • XDuce

  • Referenced in 54 articles [sw12436]
  • foundations in the theory of regular tree automata, and present a complete formal definition...
  • Antichains

  • Referenced in 29 articles [sw20208]
  • algorithm for checking universality of finite automata. We propose and evaluate a new algorithm ... checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses ... language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata...
  • IF-2.0

  • Referenced in 46 articles [sw03303]
  • intermediate representation language based on extended timed automata. In particular, this representation allowed...
  • UPPAAL TIGA

  • Referenced in 42 articles [sw12913]
  • solving games based on timed game automata with respect to reachability and safety properties. Though...
  • KeYmaera

  • Referenced in 41 articles [sw03709]
  • hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements...
  • MIO Workbench

  • Referenced in 29 articles [sw09762]
  • approach combines the advantages of both modal automata and interface automata, two dominant specification theories...
  • SPOT

  • Referenced in 25 articles [sw09473]
  • checking library using transition-based generalized Büchi automata. SPOT (SPOT produces our traces ... 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...
  • HYSDEL

  • Referenced in 38 articles [sw05200]
  • described by interconnections of linear dynamic systems, automata, if-then-else and propositional logic rules...
  • LANGAGE

  • Referenced in 36 articles [sw00501]
  • Maple packages for processing automata and finite semigroups...
  • REGAL

  • Referenced in 18 articles [sw00791]
  • library to randomly and exhaustively generate automata. The C++ library REGAL is devoted ... random and exhaustive generation of finite deterministic automata. The random generation of automata ... used for example to test properties of automata, to experimentally study average complexities of algorithms ... dealing with automata or to compare different implementations of the same algorithm. The exhaustive generation...
  • PEPS

  • Referenced in 34 articles [sw03186]
  • software tool used to analyze Stochastic Automata Networks(SAN) models. In its sequential version...