History-Dependent Nominal µ-Calculus
Clovis Eberhart1Bartek Klin2

1 National Institute of Informatics, Japan
2 University of Warsaw, Poland

LICS 2019, June 24–27

1 / 22

Example
Ap

SB
q

lockA

p

unlockB

unlockA
lockB

qr

unlockA

Can A and B both interact with critical section S at the sametime?

2 / 22

Example
Ap

SB
q

lockA

p

unlockB

unlockA
lockB

qr

unlockA

Can A and B both interact with critical section S at the sametime?
Passwords:
no repetitions
infinitely many
symmetrical2 / 22

History-dependent nominal µ-calculusµ-calculus
concise, expressive syntax
good decidability properties

Sets with atoms (a.k.a. nominal sets)
general recipe to extend framework to infinite framework
orbit-finite set: possibly infinite set, representable by finite
means

Problem
How to talk about non-repetition of values?

3 / 22

Overview of this talkAlready exists:µ-calculus,
sets with atoms,µ-calculus with atoms.
Contributions:define history-dependent nominal µ-calculus,
examples of practical use,
proof that model checking problem is decidable.

4 / 22

Kripke models
Kripke model KSet K of states,transition relation −→ ⊆ K × K ,satisfaction relation  ⊆ K × P.

ExampleTake P = {ina | a ∈ Σ} ∪ {outa | a ∈ Σ} and K:
K = Σ3 ,(b, c, d) −→ (a, b, c) for all a, b, c, d ∈ Σ,(a, b, c)  ina , (a, b, c)  outc .

5 / 22µ-calculus: syntax and semantics
Goal: prove properties of Kripke models.

Syntaxϕ ::= > | p | ¬ϕ | ϕ ∨ ϕ | 3ϕ | X | µX .ϕSemantics
Given a Kripke model K and a context ρ : X * P(K ):J3ϕKρ = {x ∈ K | ∃y ∈ JϕKρ ,J>Kρ = K ,x −→ y },JpKρ = {x ∈ K | x  p},
JX Kρ = ρ(X ),J¬ϕK = K \ JϕK ,ρρ

Jϕ ∨ ψKρ = JϕKρ ∪ JψKρ ,JµX .ϕKρ = lfp(A 7→JϕKρ[X 7→A] ).

6 / 22µ-calculus: properties

Fragments
The µ-calculus contains LTL, CTL, and CTL? .

Model checking
Given a finite K, x ∈ K , and ϕ, it is decidable whether x ∈ JϕK.

Satisfiability
Given ϕ, it is decidable whether there exists K and x ∈ K suchthat x ∈ JϕK (ϕ has a model).

7 / 22

Nominal sets
[Gabbay, Pitts, LICS 1999]

Sets with atoms“Sets” built from the emptyset and atoms from A, with finitesupport.

Examples{(a0 , a) | a ∈ A}

{ai | i even}

Equivariant function
No particular atom in definition of function.

Examplesf:

A3→ A2(a, a, b) 7→ (a, a)(a, b, c) 7→ (a, c)

f:

A2→A3
(a, a) 7→ (a, a, a0 )(a, b) 7→ (a, a, b)
8 / 22

Orbit-finite sets
Orbits of XPossible “shapes” of elements of X .

Exampleclassical set (without atoms): each element has its own shape
A: single shape
A2 : two shapes ((a, a) and (a, b) for a 6= b)
A∗ : infinitely many shapes

Proposition
Orbit-finite sets can effectively be represented by finite means.

9 / 22

The general recipe
RecipeFor 1 infinite framework:
Ingredients:
1 finite framework

12atoms3

replace “sets” by “sets with atoms”
add “equivariant” or“finitely-supported” to relations andfunctions
replace “finite” by “orbit-finite”Examples
automata with atoms [Bojańczyk, Klin, Lasota, LICS 2011]
Turing machines with atoms [Bojańczyk, Klin, Lasota, Toruńczyk,LICS 2013]µ-calculus with atoms [Klin, Lelyk, CSL 2017]10 / 22

Kripke models (with atoms)
Kripke model
Fix P set with atoms, K = (K , −→, ) with:
K set with atoms,−→ ⊆ K × K finitely-supported relation, ⊆ K × P finitely-supported relation.

BufferP = {ina | a ∈ A} ∪ {outa | a ∈ A}
K = A3 ,(b, c, d) −→ (a, b, c)(a, b, c)  ina , (a, b, c)  outc
νX .((ina → 22 outa ) ∧ 2X )11 / 22µ-calculus with atoms: syntax and semantics
From [Klin and Lelyk, CSL 2017].

Syntaxϕ ::= > | p | ¬ϕ |_ϕa | 3ϕ | X | µX .ϕa∈Awith

Wa∈A ϕa orbit-finite.

Semantics
t_a∈A

ϕa|=ρ[a∈A

Jϕa Kρ

Example^νX .((ina → 22 outa ) ∧ 2X )a∈A
12 / 22µ-calculus with atoms: properties

Model checking
Given an orbit-finite K, x ∈ K , and ϕ, it is decidable whetherx ∈ JϕK.

Satisfiability
Given ϕ, it is undecidable whether ϕ has a model.

Fragments
The µ-calculus with atoms does not contain atomic CTL? .

13 / 22

#Path#Path: “there exists a path on which no predicate holds morethan once”.

Problem#Path not definable in µ-calculus with atoms.
Useful property for verification:“if no password is used twice, the protocol behaves well”,“does there exist a path where predicates hold at most onceand property P is violated?”

Frustrating#Path definable in atomic CTL? . . . but model checking
problem undecidable,#Path decidable!
14 / 22

Example: critical section
ApS

B
q

lockA

punlockB

unlockA
lockB

qr

unlockA

Possible models:remember all generated passwords: property expressible inµ-calculus with atoms, model orbit-infinite,
don’t remember anything: model orbit-finite, property not
expressible in µ-calculus with atoms.
15 / 22

Example: critical section (formal)

Predicates{pa | a ∈ A} ∪ {lockA , lockB , unlockA , unlockB }Statesx = (aA , aB , aS , s, t) withaX ∈ A or aX = ∅,s ∈ {p, lock, unlock, ∅},t ∈ {A, B, ∅}.

16 / 22

Example: Needham–Schroeder protocol
AnA

B(nA , A)kPB

AnAE

B

(nA , A)kPE

nA

A, nAnB(nA , A)kPB(nA , nB )kPA

nA , nB(nB )kPB

A, nAnB(nA , nB )kPAnBnA , nB(nA , nB )kPA

(nB )kPEnB(nB )kPB

nB

17 / 22

History-dependent nominal µ-calculus
Syntaxϕ ::= > | pa | ¬ϕ |_ϕa | 3ϕ | X | µX .ϕ | ]aa∈ASemantics
Need to track history H of encountered atoms:
JµX .ϕKρ = lfp(A 7→x ∈ J3ϕKH
ρ iff thereexists
JϕKρ[X 7→A] ),x −→ y ∈ JϕKH∪evt(x),ρ∅ if a ∈ HJ]aKH
Hρ =K otherwise
JX Kρ = ρ(X )(H),#Path!
#Path = νX .

^(pa → ]a) ∧ 3X

a∈A
18 / 22

Example: critical section“Good” paths
safe =^(pa → ]a)a∈A

Property of interest
PA = νX .(safe → (unlockA ∨ (¬unlockB ∧ 2X )))νX .(safe → ((lockA → PA ) ∧ (lockB → PB ) ∧ 2X ))19 / 22

Model checking

Question
Is model checking decidable on orbit-finite models?

Problem
Computing semantics of fixpoints:µ-calculus: compute inductively from ⊥, stabilises byKnaster-Tarski (JµX .ϕKρ ⊆ K finite),µ-calculus with atoms: idem, stabilises for similar reasons,here: JµX .ϕKρ function of history H, no similar techniqueapplies.

20 / 22

Forgetful semantics
Idea
Define LϕMn,Hsuch that:
ρLϕMρn,H computable,0n,HJϕKH,
ρ computable from LϕMρ

H remains bounded when computing LϕMn,Hρ .

Answer0∪HLϕMn,H
like JϕKH, where H only contains atoms relevant to ϕρρand ρ and the current state.

TheoremFor any closed formula ϕ, JϕK∅∅ = LϕM0,∅∅ .
21 / 22

Conclusion
Done
defined µ-calculus with atoms and “atom freshness”
proves useful for verification
model checking is decidable

Limit of decidability]p for predicates with general supports (> 1 elements) undecidable.

To-dovectorial µ-calculus
links to alternating tree automata and parity games
other atoms (e.g., ordered) ; probably undecidable

22 / 22Conclusion
Donedefined µ-calculus with atoms and “atom freshness”
proves useful for verification
model checking is decidable

Limit of decidability]p for predicates with general supports (> 1 elements) undecidable.

To-dovectorial µ-calculus
links to alternating tree automata and parity games
other atoms (e.g., ordered) ; probably undecidable
Thank you for your attention.
22 / 22