Compositional verification of concurrent systems by combining bisimulations
From MaRDI portal
Publication:2147689
DOI10.1007/S10703-021-00360-WOpenAlexW4231183851MaRDI QIDQ2147689FDOQ2147689
Authors: Frédéric Lang, Radu Mateescu, Franco Mazzanti 
Publication date: 20 June 2022
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-03159616v2/file/Lang-Mateescu-Mazzanti-21.pdf
Recommendations
- Compositional verification of concurrent systems by combining bisimulations
- Sharp congruences adequate with temporal logics combining weak and strong modalities
- Automatic verification of concurrent systems using a formula-based compositional approach
- Compositionality and locality for improving model checking in the selective mu-calculus
- Compositional verification of asynchronous concurrent systems using CADP
model checkingtemporal logicstate space reductionconcurrency theorymodal mu-calculuslabelled transition system
Cites Work
- Derivatives of Regular Expressions
- Propositional dynamic logic of regular programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Compositional verification of asynchronous concurrent systems using CADP
- Propositional dynamic logic of looping and converse is elementarily decidable
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Results on the propositional \(\mu\)-calculus
- Branching time and abstraction in bisimulation semantics
- Modeling and analysis of communicating systems
- An automata theoretic decision procedure for the propositional mu- calculus
- Three logics for branching bisimulation
- Title not available (Why is that?)
- Sequential and distributed on-the-fly computation of weak tau-confluence
- Title not available (Why is that?)
- Confluence for process verification
- A partial order approach to branching time logic model checking.
- Title not available (Why is that?)
- Partial model checking using networks of labelled transition systems and Boolean equation systems
- Sharp congruences adequate with temporal logics combining weak and strong modalities
- Partial-order reduction in the weak modal mu-calculus
Cited In (8)
- Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
- Compositional verification of concurrent systems by combining bisimulations
- On the complexity of verifying concurrent transition systems
- Title not available (Why is that?)
- \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics
- A Proof System for Compositional Verification of Probabilistic Concurrent Processes
- On the computation of counterexamples in compositional nonblocking verification
- Deriving Bisimulation Congruences for Conditional Reactive Systems
Uses Software
This page was built for publication: Compositional verification of concurrent systems by combining bisimulations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147689)
