Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: Modal Logics for Nominal Tran...


view this post on Zulip Email Gateway (Aug 22 2022 at 14:23):

From: Tobias Nipkow <nipkow@in.tum.de>
Modal Logics for Nominal Transition Systems
Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström and
Ramunas Gutkovas

We formalize a uniform semantic substrate for a wide variety of process calculi
where states and action labels can be from arbitrary nominal sets. A
Hennessy-Milner logic for these systems is defined, and proved adequate for
bisimulation equivalence. A main novelty is the construction of an infinitary
nominal data type to model formulas with (finitely supported) infinite
conjunctions and actions that may contain binding names. The logic is
generalized to treat different bisimulation variants such as early, late and
open in a systematic way.

https://www.isa-afp.org/entries/Modal_Logics_for_NTS.shtml

Enjoy!
smime.p7s


Last updated: Apr 25 2024 at 08:20 UTC