mCRL2

swMATH1496MaRDI QIDQ14230

No author found.

Related Items (59)

A set automaton to locate all pattern matches in a term ⋮ Theorem proving graph grammars with attributes and negative application conditions ⋮ Abstraction in Fixpoint Logic ⋮ An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation ⋮ Family-Based SPL Model Checking Using Parity Games with Variability ⋮ Analysing sanity of requirements for avionics systems ⋮ Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types ⋮ Specification Guidelines to Avoid the State Space Explosion Problem ⋮ Saving Space in a Time Efficient Simulation Algorithm ⋮ Unnamed Item ⋮ Axiomatizing recursion-free, regular monitors ⋮ An efficient algorithm to determine probabilistic bisimulation ⋮ Model Checking Value-Passing Modal Specifications ⋮ Term rewriting on GPUs ⋮ Input-output conformance testing for software product lines ⋮ Combine and conquer: relating BIP and Reo ⋮ An Overview of the mCRL2 Toolset and Its Recent Advances ⋮ Symbolic Analysis Tools for CSP ⋮ Off-the-shelf automated analysis of liveness properties for just paths ⋮ Interface automata for shared memory ⋮ Revisiting sequential composition in process calculi ⋮ A formalisation of consistent consequence for Boolean equation systems ⋮ Logical characterisations, rule formats and compositionality for input-output conformance simulation ⋮ Product line process theory ⋮ Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions ⋮ Verification of distributed systems with the axiomatic system of MSVL ⋮ Decomposing monolithic processes in a process algebra with multi-actions ⋮ Symbolic execution of Reo circuits using constraint automata ⋮ A generic framework for \(n\)-protocol compatibility checking ⋮ Extended beam search for non-exhaustive state space analysis ⋮ Modeling and verification of reconfigurable printing system based on process algebra ⋮ From generic partition refinement to weighted tree automata minimization ⋮ Strategies, model checking and branching-time properties in Maude ⋮ A formal verification technique for behavioural model-to-model transformations ⋮ Invariants for parameterised Boolean equation systems ⋮ A Multi-Core Solver for Parity Games ⋮ Dynamic consistency in process algebra: from paradigm to ACP ⋮ Lifting non-finite axiomatizability results to extensions of process algebras ⋮ Consistent Correlations for Parameterised Boolean Equation Systems with Applications in Correctness Proofs for Manipulations ⋮ A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus ⋮ Verification of mobile ad hoc networks: an algebraic approach ⋮ Dynamic Consistency in Process Algebra: From Paradigm to ACP ⋮ Synchronous Kleene algebra ⋮ Verification of reactive systems via instantiation of parameterised Boolean equation systems ⋮ An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation ⋮ Verification of Context-Dependent Channel-Based Service Models ⋮ Suitability of mCRL2 for Concurrent-System Design: A 2 × 2 Switch Case Study ⋮ A Formal Calculus for Informal Equality with Binding ⋮ Unnamed Item ⋮ A formal semantics of extended hierarchical state transition matrices using CSP\# ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Branching Bisimulation Games ⋮ Analysing an autonomous tramway positioning system with the \textsc{Uppaal} statistical model checker ⋮ Improving parity game solvers with justifications ⋮ Instantiation for Parameterised Boolean Equation Systems ⋮ Conceptual building blocks for modeling reconfiguration of component-based systems using Petri nets ⋮ Lifted structural invariant analysis of Petri net product lines ⋮ Off-the-shelf automated analysis of liveness properties for just paths (extended abstract)

This page was built for software: mCRL2