Symbolic Bisimulation for Open and Parameterized Systems
summary
Covers symbolic bisimulation techniques applied to open and parameterized systems, focusing on methods to reason about behavioral equivalence in systems with free variables or parameters. Discusses how symbolic representations and algorithms can handle state spaces that depend on unknown or varying components.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:28Open Systems
- 1:40Background: distributed components, the pNet model, and the Vercors platform
- 3:29So... Let's go symbolic and compositional?
- 5:31The (open) pNet model: Structure, synchronisation
- 7:20pNet semantics: Open Transitions, Open automata
- 8:31Running example: Enable operator
- 9:19Running example: encodings of Enable (1)
- 11:25FH-bisimulation (Forte 2016)
- 13:25FH-Bisimulation: Properties
- 14:17Semantic Open Automata & FH-bisimulation
- 16:11Algorithm 1: Check a given Bisimulation
- 17:48Algo 1: Check Bisimulation
- 18:44Check Bisimulation, Properties
- 19:51Algorithm 2
- 21:00On-the-fly Bisimulation - Key point
- 22:28Conclusion and perspectives
related talks
22mCategorical Semantics of Probabilistic Symbolic Execution
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
16mCompositional Symbolic Execution for the Next 700 Memory Models
37mClassical Processes in modern dress
23mLet Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)
18mPsym: Efficient Symbolic Exploration of Distributed Systems
15mClosing Remarks
27mParameterized Infinite-State Reactive Synthesis