Introducing 

Prezi AI.

Your new presentation assistant.

Refine, enhance, and tailor your content, source relevant images, and edit visuals quicker than ever before.

Loading…
Transcript

Bisimilarity

Linear time

branching time

2-nested similarity

Spectrum

Ready similarity

Ready traces

Possible futures

Rob van Glabbeek

Failure traces

Readies

(2,2,0,0,1,1)

Implication

Observations

Games everywhere!

Impossible futures

Revivals

Similarity

3 Observations

3 Conjunctions

2 Main positive height

1 Other positive height

1 Negation height

1 Negations

Failures

Pricing

Tom Henzinger Fest Workshop @ CAV 2023-07-18

(2,2,0,0,1,1)

(2,2,1,1,0,0)

Distinguishing

HML-Formulas

Traces

Simulated by?

“How much

Distinction Power

To tell two systems apart?”

Bisimilar?

Transition

Systems

Finest

Preorders

benjamin.bisping@tu-berlin.de

bbisping.de

Failure-

Trace-equivalent/preordered?

Decide All

from the spectrum

Games to

Behavioral Equivalences

at Once

Exponential size

+ Linear Branching-Degree

Bisimilarity

⟨a⟩⋀{..., ...}

Just one

quantitative problem!

Generalized bisimulation game

Using an energy game

No major complexity overhead!

price domination

pruning

⟨a⟩...

Defender

Attacker

-1,0,0,0,0,0

...on

https://equiv.io!

a, p', q

Simulation

⋀{..., ...}

min[1,3],0,0,0,0,0

symmetry

¬ ...

0,-1,0,0,0,0

No traces :(

TACAS'21

CAV'23

(draft)

LMCS'22

min[1,4],0,0,0,0,0

0,0,0,min[3,4],0,0

Uwe Nestmann

David N. Jansen

min[1,5],0,0,0,0,-1

Observations

Conjunctions

Attacker wins

Main positive height

Other positive height

Traces

& more :)

Negation height

¬ ...

Defender Wins

Negations

Colin Stirling

Pareto frontier of attacker wins

Spectroscopy

Game

Bisimulation

Game

Attacker Winning Region

Attacker Winning Energy Budgets

Energy

Exponential wrt. Branching-degree

Exponential

wrt. Size

& Cheapest Formulas

Learn more about creating dynamic, engaging presentations with Prezi