
UMDES
 Referenced in 390 articles
[sw09523]
 discrete event systems modeled by finitestate automata (FSA). There are routines for the manipulation...

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

Kronos
 Referenced in 273 articles
[sw01270]
 realtime systems are modeled by timed automata and the correctness requirements are expressed...

MONA
 Referenced in 133 articles
[sw06170]
 years, including formula reductions, DAGification, guided tree automata, threevalued logic, eager minimization, BDDbased ... automata representations, and cacheconscious data structures. We describe these techniques and quantify their respective...

Esterel
 Referenced in 165 articles
[sw20012]
 systems, including realtime systems and control automata. The Esterel v5 compiler can be used...

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

Timbuk
 Referenced in 47 articles
[sw06351]
 Term Rewriting Systems and for manipulating Tree Automata (bottomup nondeterministic 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 automatabased models equipped with variables belonging to different infinite/finite ... present time, parametric (continuoustime) timed automata, extended with integer counters and finitedomain variables...

VerICS
 Referenced in 35 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 Kronoslike 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...

Antichains
 Referenced in 33 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 ... languageinclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata...

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

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

UPPAAL TIGA
 Referenced in 45 articles
[sw12913]
 solving games based on timed game automata with respect to reachability and safety properties. Though...

KeYmaera
 Referenced in 44 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 transitionbased generalized Büchi automata. SPOT (SPOT produces our traces ... relies on transitionbased 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...

LANGAGE
 Referenced in 39 articles
[sw00501]
 Maple packages for processing automata and finite semigroups...

HYSDEL
 Referenced in 39 articles
[sw05200]
 described by interconnections of linear dynamic systems, automata, ifthenelse and propositional logic rules...

QCADesigner
 Referenced in 25 articles
[sw22781]
 simulation tool for quantumdot cellular automata. QCADesigner is the product of an ongoing research ... simulation tool for Quantum Dot Cellular Automata (QCA). This tool is still under development...

PGSolver
 Referenced in 35 articles
[sw14051]
 infinite duration that have important applications in automata theory and decision procedures (validity as well...