History-dependent mu-calculus

Motto: Those who cannot remember the past are free to reinvent it.

Abstract: Mu-calculus with atoms extends the classical mu-calculus

with orbit-finitary boolean operators, to describe properties of transition

systems with atoms. Its expressivity leaves much to be desired:

the property "there exists an infinite path where no atom appears

more than once" cannot be defined in it. I will say how the calculus

can be extended with simple atom freshness tests so that the property

becomes definable. It is not clear at all whether model-checking

for this extended calculus remains decidable, but we prove that it does.