• Petri-PDL

  • Referenced in 3 articles [sw15081]
  • formally designed following the representation of Kripke models as rewrite theories defined for the Linear...
  • Spin-to-Grape

  • Referenced in 6 articles [sw07515]
  • examples of Promela models of concurrent, distributed systems, whose associated Kripke structures have more complex ... allows the state-graph of a Promela model to be manipulated using the group-theoretic ... system and the symmetry group of the Kripke structure associated with the system. We then ... describe the symmetry groups of the associated models. Finally we discuss ways in which symmetry...
  • VPM

  • Referenced in 11 articles [sw07364]
  • mapping from UML models to different semantic domains (Petri nets, Kripke automaton, process algebras ... structure and operational semantics of mathematical models can be defined in a UML notation without...
  • GOALIE

  • Referenced in 1 article [sw30043]
  • Common Lisp Application to Discover Kripke Models: Redescribing Biological Processes from Time-Course Data...
  • LoTREC

  • Referenced in 25 articles [sw07684]
  • tableaux system for building models or counter-models and testing satisfiability of formulas in modal ... strategies. It aims at covering all Kripke-semantic based logics. It is implemented in Java...
  • TSMV

  • Referenced in 2 articles [sw13326]
  • protocols, etc. The underlying model is an extension of Kripke structures, where every transition carries...
  • ACTLW

  • Referenced in 7 articles [sw21031]
  • based computation tree logic with unless operator. Model checkers for systems represented by labelled transition ... used as those for systems represented by Kripke structures. This is partially ... operators together with symbolic algorithms for global model checking are shown. Usage of this...
  • Orchids

  • Referenced in 3 articles [sw09807]
  • based on techniques for fast, on-line model-checking. Temporal formulae are taken from ... event flows, which together form a linear Kripke structure...
  • Coq

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

  • Referenced in 71 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • Isabelle

  • Referenced in 674 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Ott

  • Referenced in 31 articles [sw00663]
  • Semantic definitions of full-scale programming languages are...
  • SIGREF

  • Referenced in 15 articles [sw00859]
  • We present a uniform signature-based approach to...
  • PRISM

  • Referenced in 434 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper...
  • HiLog

  • Referenced in 49 articles [sw01580]
  • HiLog: A foundation for higher-order logic programming...
  • ConGolog

  • Referenced in 48 articles [sw01801]
  • ConGolog, a concurrent programming language based on the...
  • JoCaml

  • Referenced in 26 articles [sw02065]
  • JoCaml: A language for concurrent distributed and mobile...
  • GOLOG

  • Referenced in 170 articles [sw02159]
  • GOLOG: A logic programming language for dynamic domains...