Compositionality in state space verification methods

DOI10.1007/3-540-61363-3_3zbMATH Open1418.68155OpenAlexW2098418324MaRDI QIDQ4633153FDOQ4633153

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

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

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)

Cites Work

• 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?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CCS expressions, finite state processes, and three problems of equivalence
• A Theory of Communicating Sequential Processes
• Minimizing the number of transitions with respect to observation equivalence
• An implementation of an efficient algorithm for bisimulation equivalence
• Three logics for branching bisimulation
• Testing equivalence as a bisimulation equivalence
• Acceptance trees
• Compositional failure-based semantic models for basic LOTOS
• Title not available (Why is that?)
• The weakest deadlock-preserving congruence
• A partial order approach to branching time logic model checking.
• 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?)

Cited In (11)

• To compose, or not to compose, that is the question: an analysis of compositional state space generation
• Compositional checking of satisfaction
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• On compositionality and its limitations
• Title not available (Why is that?)
• On the computation of counterexamples in compositional nonblocking verification
• Compositional reasoning

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)