scientific article

Olaf Burkart, Bernhard Steffen, Didier Caucal, Faron Moller

Publication date: 2001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

process algebra model checking bisimulation parallel processes equivalence testing branching time logic linear time logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (48)

Bounded situation calculus action theories ⋮ Model independent approach to probabilistic models ⋮ Bounded model checking of infinite state systems ⋮ Progression and verification of situation calculus agents with bounded beliefs ⋮ Partially-Commutative Context-Free Processes ⋮ Complete symbolic reachability analysis using back-and-forth narrowing ⋮ Decidability issues for extended ping-pong protocols ⋮ A generic framework for checking semantic equivalences between pushdown automata and finite-state automata ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Characteristic invariants in Hennessy-Milner logic ⋮ CCS with Replication in the Chomsky Hierarchy: The Expressive Power of Divergence ⋮ Theory of interaction ⋮ Simulation relations and applications in formal methods ⋮ The complexity of bisimilarity-checking for one-counter processes. ⋮ Reasoning about sequences of memory states ⋮ On Recursion, Replication and Scope Mechanisms in Process Calculi ⋮ Complexity of deciding bisimilarity between normed BPA and normed BPP ⋮ Selected Ideas Used for Decidability and Undecidability of Bisimilarity ⋮ Normed BPA vs. Normed BPP Revisited ⋮ Compositional verification of sequential programs with procedures ⋮ Sequencing and intermediate acceptance: Axiomatisation and decidability of bisimilarity ⋮ Undecidability of performance equivalence of Petri nets ⋮ Bouziane's transformation of the Petri net reachability problem and incorrectness of the related algorithm ⋮ An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems ⋮ Turing Machines, Transition Systems, and Interaction ⋮ Partially-commutative context-free processes: expressibility and tractability ⋮ Deciding probabilistic bisimilarity over infinite-state probabilistic systems ⋮ Weak bisimilarity and regularity of context-free processes is EXPTIME-hard ⋮ Turing machines, transition systems, and interaction ⋮ On the computational complexity of bisimulation, redux ⋮ Normed Processes, Unique Decomposition, and Complexity of Bisimulation Equivalences ⋮ On Decidability of LTL+Past Model Checking for Process Rewrite Systems ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Unnamed Item ⋮ A brief history of process algebra ⋮ On the complexity of checking semantic equivalences between pushdown processes and finite-state processes ⋮ A general approach to comparing infinite-state systems with their finite-state specifications ⋮ Decidability of performance equivalence for basic parallel processes ⋮ Model checking for process rewrite systems and a class of action-based regular properties ⋮ Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems ⋮ Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems ⋮ Reachability is decidable for weakly extended process rewrite systems ⋮ Types and trace effects for object orientation ⋮ Bisimilarity on basic parallel processes ⋮ Decidable first-order transition logics for PA-processes ⋮ Simulation preorder over simple process algebras ⋮ Narrowing and Rewriting Logic: from Foundations to Applications

This page was built for publication: