Refinement sensitive formal semantics of state machines with persistent choice

DOI10.1016/J.ENTCS.2009.08.006MaRDI QIDQ2810972zbMATH OpenOpenAlexFDO

Authors Michael Huth, Heiko Schmidt, Jens Schönborn, Harald Fecher

Publication date 6 June 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.08.006

zbMATH Keywords

3-valued satisfaction\(\mu\)-calculusformal semanticsmodeling languagenondeterminism

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Refinement Patterns for Hierarchical UML State Machines
• Concurrency and refinement in the unified modeling language
• scientific article; zbMATH DE number 2080017
• scientific article; zbMATH DE number 1670514
• Algebraic Methodology and Software Technology

Cites work

• 3-valued abstraction: More precision at less cost
• A logic for reasoning about time and reliability
• A probabilistic extension of UML statecharts specification and verification
• Alternating tree automata, parity games, and modal -calculus
• Automata for the modal -calculus and related results
• Bisimulation can't be traced
• Concurrency and refinement in the unified modeling language
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• Probability and Nondeterminism in Operational Models of Concurrency
• Process algebra having inherent choice: revised semantics for concurrent systems
• Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise
• Results on the propositional \(\mu\)-calculus
• Statecharts: a visual formalism for complex systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Underspecification, inherent nondeterminism and probability in sequence diagrams
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Model Checking for Action Abstraction

This page was built for publication: Refinement sensitive formal semantics of state machines with persistent choice

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