Simulation relations and applications in formal methods

DOI10.1007/978-3-031-22337-2_13MaRDI QIDQ6113980zbMATH OpenOpenAlexFDO

Authors Kim G. Larsen, Christian Schilling, Jiří Srba

Publication date 10 August 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-22337-2_13

zbMATH Keywords

automata theorybisimulationhybrid systemsimulationtransition system

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Equivalence checking 40 years after: a review of bisimulation tools
• Refinement checking based on simulation relations
• Tools and Algorithms for the Construction and Analysis of Systems
• Bisimulation and Simulation Relations for Markov Chains
• Hybrid automata and bisimulations

Cites work

• 20 years of modal and mixed specifications.
• A theory of timed automata
• A uniform (bi-)simulation-based framework for reducing tree automata
• Abstraction and abstraction refinement
• Abstractions for hybrid systems
• Advanced automata minimization
• Algorithmic analysis of nonlinear hybrid systems
• Approximate equivalence and synchronization of metric transition systems
• Approximate simulation relations for hybrid systems
• Approximately bisimilar symbolic models for nonlinear control systems
• Approximation Metrics for Discrete and Continuous Systems
• Beyond hyper-minimisation -- minimising DBAs and DPAs is NP-complete
• Beyond Language Equivalence on Visibly Pushdown Automata
• Büchi automata can have smaller quotients
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
• Complexity of Decision Problems for Mixed and Modal Specifications
• CONCUR 2005 – Concurrency Theory
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• Equivalence-checking with infinite-state systems: techniques and results
• EXPTIME-complete decision problems for modal and mixed specifications
• Fair simulation
• Fair simulation for nondeterministic and probabilistic Büchi automata: a coalgebraic perspective
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• FDR3 -- a modern refinement checker for CSP
• From bisimulation to simulation: Coarsest partition problems
• From timed automata to logic -- and back
• scientific article; zbMATH DE number 1614700 (Why is no real title available?)
• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 176736 (Why is no real title available?)
• scientific article; zbMATH DE number 177515 (Why is no real title available?)
• scientific article; zbMATH DE number 177824 (Why is no real title available?)
• scientific article; zbMATH DE number 3460178 (Why is no real title available?)
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• scientific article; zbMATH DE number 1306878 (Why is no real title available?)
• scientific article; zbMATH DE number 1332671 (Why is no real title available?)
• scientific article; zbMATH DE number 1927559 (Why is no real title available?)
• scientific article; zbMATH DE number 1927588 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 1538045 (Why is no real title available?)
• scientific article; zbMATH DE number 1759609 (Why is no real title available?)
• scientific article; zbMATH DE number 2155191 (Why is no real title available?)
• scientific article; zbMATH DE number 1903384 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Hybrid automata with finite bisimulations
• Infinite Games
• Infinite results
• Minimal NFA Problems are Hard
• Minimization of visibly pushdown automata is NP-complete
• Minimization of visibly pushdown automata using partial Max-SAT
• Minimizing Generalized Büchi Automata
• On determinism in modal transition systems
• On Modal Refinement and Consistency
• On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract)
• Parametric modal transition systems
• Process rewrite systems.
• Property preserving abstractions for the verification of concurrent systems
• Reactive Systems
• State equivalences for rectangular hybrid automata
• Taylor approximation for hybrid systems
• The algorithmics of bisimilarity
• The existence of refinement mappings
• Three Partition Refinement Algorithms
• Time-abstracted bisimulation: Implicit specifications and decidability
• Transformational design and implementation of a new efficient solution to the ready simulation problem
• Undecidability of bisimilarity by defender's forcing
• Uppaal in a nutshell
• Verification on infinite structures.
• Visibly pushdown languages
• What's decidable about hybrid automata?

Cited in

(6)

• Fixpoint semantics and simulation
• A modular approach to defining and characterising notions of simulation
• Refinement checking based on simulation relations
• Mathematical Foundations of Computer Science 2003
• Equivalence checking 40 years after: a review of bisimulation tools
• On simulation and propagating EOL forms

This page was built for publication: Simulation relations and applications in formal methods

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