Model refinement using bisimulation quotients

DOI10.1007/978-3-642-17796-5_5MaRDI QIDQ3067468zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Roland Glück, Bernhard Möller, Michel Sintzoff

Publication date 21 January 2011

Published in Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL https://opus.bibliothek.uni-augsburg.de/opus4/frontdoor/index/index/docId/58784

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Using bisimulations for optimality problems in model refinement
• Refinement is complete for implementations
• Hybrid automata and bisimulations
• Bisimulation and action refinement
• Verification of infinite-state dynamic systems using approximate quotient transition systems

Cites work

• A classification of symbolic transition systems
• A semiring approach to equivalences, bisimulations and control
• CCS expressions, finite state processes, and three problems of equivalence
• Equivalence notions and model minimization in Markov decision processes
• Graphs, dioids and semirings. New models and algorithms.
• scientific article; zbMATH DE number 701387 (Why is no real title available?)
• scientific article; zbMATH DE number 1142329 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Synthesis of Optimal Control Policies for Some Infinite-State Transition Systems

Cited in

(8)

• Isolated sublattices and their application to counting closure operators
• Two observations in dioid based model refinement
• Using bisimulations for optimality problems in model refinement
• Bisimulations and bisimulation quotients of generalized Veltman models
• scientific article; zbMATH DE number 2119841 (Why is no real title available?)
• Compatibility of refining and controlling plant automata with bisimulation quotients
• Isolated suborders and their application to counting closure operators
• A matrix-oriented view of bisimulation quotients over dioid-labeled transition systems

This page was built for publication: Model refinement using bisimulation quotients

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