Compositionality in state space verification methods

DOI10.1007/3-540-61363-3_3MaRDI QIDQ4633153zbMATH OpenOpenAlexFDO

Authors Antti Valmari

Publication date 2 May 2019

Published in Application and Theory of Petri Nets 1996 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61363-3_3

zbMATH Keywords

labeled transition systemparallel compositiontrace semanticserror indicationdivergence trace

Mathematics Subject Classification ID

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

Recommendations

• Compositional Verification of Quantitative Properties of Statecharts
• scientific article; zbMATH DE number 1487866
• Compositional Verification for Component-Based Systems and Application
• Compositional analysis for verification of parameterized systems
• scientific article; zbMATH DE number 1956590
• Verification of large state/event systems using compositionality and dependency analysis
• scientific article; zbMATH DE number 1444724
• A compositional approach to the verification of hybrid systems
• Compositional semantics and refinement of Statecharts

Cites work

• scientific article; zbMATH DE number 3852428 (Why is no real title available?)
• scientific article; zbMATH DE number 4199644 (Why is no real title available?)
• scientific article; zbMATH DE number 3902016 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 58291 (Why is no real title available?)
• scientific article; zbMATH DE number 177239 (Why is no real title available?)
• scientific article; zbMATH DE number 177845 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 4119652 (Why is no real title available?)
• A Theory of Communicating Sequential Processes
• A partial order approach to branching time logic model checking.
• Acceptance trees
• An implementation of an efficient algorithm for bisimulation equivalence
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CCS expressions, finite state processes, and three problems of equivalence
• Compositional failure-based semantic models for basic LOTOS
• Minimizing the number of transitions with respect to observation equivalence
• Testing equivalence as a bisimulation equivalence
• The weakest deadlock-preserving congruence
• Three logics for branching bisimulation

Cited in

(11)

• To compose, or not to compose, that is the question: an analysis of compositional state space generation
• Compositional checking of satisfaction
• scientific article; zbMATH DE number 1746446 (Why is no real title available?)
• External behaviour of systems of state machines with variables
• State Space Representation for Verification of Open Systems
• Selective mu-calculus and formula-based equivalence of transition systems
• scientific article; zbMATH DE number 7407780 (Why is no real title available?)
• On compositionality and its limitations
• scientific article; zbMATH DE number 1754684 (Why is no real title available?)
• On the computation of counterexamples in compositional nonblocking verification
• Compositional reasoning

Describes a project that uses

Uses Software

• LOTOS

This page was built for publication: Compositionality in state space verification methods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4633153)