stutter bisimulation

In Principles of Model Checking, Baier and Katoen define a stutter bisimulation for a single transition system and later adapt it to a relation on two transition systems. A stutter bisimulation for $\backslash text\{TS\}=(S,\; \backslash text\{Act\},\; \backslash to,\; I,\; \backslash text\{AP\},\; L)$ is a binary relation R on S such that for all (s₁,s₂) in R:

1. $s\_1,\; s\_2$ have the same labels
2. If $s\_1\backslash to\; s\_1\text{'}$ is a valid transition and $(s\_1\text{'},s\_2)\backslash not\backslash in\; R$ then there exists a finite path fragment $s\_2u\_1\backslash cdots\; u\_n\; s\_2\text{'}$ ($n\backslash ge\; 0$) such that each pair $(s\_1,\; u\_i)$ is in R and $(s\_1\text{'},s\_2\text{'})$ is in R
3. If $s\_2\backslash to\; s\_2\text{'}$ is a valid transition and $(s\_1,s\_2\text{'})\backslash not\backslash in\; R$ is not then there exists a finite path fragment $s\_1v\_1\backslash cdots\; v\_n\; s\_1\text{'}$ ($n\backslash ge\; 0$) such that each pair $(v\_i,\; s\_2)$ is in R and $(s\_1\text{'},s\_2\text{'})$ is in R

A generalization, the divergent stutter bisimulation, can be used to simplify the state space of a system with the tradeoff that statements using the linear temporal logic operator "next" may change truth value.{{cite journal|title=Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications|journal=Automatica|volume=130|year=2021|doi=10.1016/j.automatica.2021.109723|hdl=10289/14366|hdl-access=free |last1=Mohajerani |first1=Sahar |last2=Malik |first2=Robi |last3=Wintenberg |first3=Andrew |last4=Lafortune |first4=Stéphane |last5=Ozay |first5=Necmiye }} A robust stutter bisimulation allows uncertainty over transitions in the system.{{cite journal|title=Robust stutter bisimulation for abstraction and controller synthesis with disturbance|journal=Automatica|volume=160|year=2024|doi=10.1016/j.automatica.2023.111394|doi-access=free |last1=Krook |first1=Jonas |last2=Malik |first2=Robi |last3=Mohajerani |first3=Sahar |last4=Fabian |first4=Martin |hdl=10289/16942 |hdl-access=free }}

{{reflist}}

{{comp-sci-stub}}

Category:Transition systems