• GOAL

  • Referenced in 7 articles [sw21229]
  • logics that are expressively equivalent to these automata. Therefore, the GOAL tool will constantly...
  • TravMC2

  • Referenced in 4 articles [sw20008]
  • properties specified using alternating parity tree automata (or equivalently monadic second order logic). Our experimental...
  • MSO_Regex_Equivalence

  • Referenced in 7 articles [sw32230]
  • reduced to the equivalence of some regular structures (e.g. automata). We verify an executable decision ... based on automata but on regular expressions. Decision procedures for regular expression equivalence have been...
  • Regular Sets

  • Referenced in 14 articles [sw28793]
  • executable equivalence checker for regular expressions is verified; it does not need automata but works ... intersection are also defined and an equivalence checker is provided...
  • HyLAA

  • Referenced in 3 articles [sw20821]
  • first tool for simulation-equivalent reachability for hybrid automata with affine dynamics. HyLAA’s analysis...
  • mut-learn

  • Referenced in 1 article [sw34636]
  • implementation of an equivalence testing approach for active automata learning ... implemented as an equivalence oracle for the automata-learning library LearnLib. Basically, test-cases...
  • SPeeDI

  • Referenced in 7 articles [sw00896]
  • equivalent with respect to reachability. This is the case for classes of rectangular automata...
  • LALBLC

  • Referenced in 4 articles [sw09901]
  • LALBLC: a program testing the equivalence of DPDA’s. We describe the program LALBLC which ... tests whether two deterministic pushdown automata recognize the same language...
  • HECTOR

  • Referenced in 2 articles [sw13320]
  • knowledge, Hector is the first fully-automated equivalence checker for higher-order, call-by-value ... construct, on-the-fly, visibly pushdown automata which precisely ... capture program behaviour. These automata are then checked for language equivalence, and if they...
  • HOMER

  • Referenced in 5 articles [sw13321]
  • Model checkER. We present Homer, an observational-equivalence model checker for the 3rd-order fragment ... their game semantics as visibly pushdown automata (VPA). The VPA-translates are then passed ... which we have implemented) to test for equivalence. Thanks to the fully abstract game semantics...
  • DEQ

  • Referenced in 0 articles [sw34234]
  • Equivalence Checker for Deterministic Register Automata. Register automata are one of the most studied automata ... verification. We present an equivalence checker for deterministic register automata, called DEQ, based...
  • WNetKAT

  • Referenced in 1 article [sw25228]
  • WNetKAT and the equivalence problem of the weighted finite automata, which implies undecidability...
  • Regex_Equivalence

  • Referenced in 6 articles [sw32229]
  • verified decision procedures for regular expression equivalence. Five recently published formalizations of such decision procedures ... seems to produce uniformly smaller automata. The common framework makes it possible to compare...
  • Limi

  • Referenced in 4 articles [sw20206]
  • takes as input two non-deterministic finite automata (NFA) A and B with a shared ... independent. Two strings of the language are equivalent module independence if they are identical...
  • biXid

  • Referenced in 9 articles [sw12667]
  • treating formats that do not have equivalent expressivenesses, and (3) allow non-linear pattern variables ... phases use a variant of finite tree automata for performing a one-pass scan...
  • LTL_to_GBA

  • Referenced in 1 article [sw29245]
  • convert LTL formulas to generalized Büchi automata. We also formalize some syntactic rewrite rules that ... before conversion. Moreover, we integrate the Stuttering Equivalence AFP-Entry by Stefan Merz, adapting...
  • PESTS

  • Referenced in 2 articles [sw35864]
  • implements the algorithm for quotienting finite-state automata introduced in the paper: Gabriele Costa, David ... common setting, the two are equivalent. Aside from their theoretical interest, our results build ... partial model checking of finite-state automata that can be used as an alternative...
  • multiPDEVS

  • Referenced in 1 article [sw30698]
  • construction showing that any multiPDEVS model is equivalent to a PDEVS atomic model. We then ... well-adapted formalism to express cellular automata, we finally propose to compare an implementation...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • demands for advanced validation techniques. Hybrid automata are a clean and consolidated formal language ... language is automatically compiled into equivalent discrete-time infinite-state transition systems...
  • Coq

  • Referenced in 1828 articles [sw00161]
  • Coq is a formal proof management system. It...