# Modal Logics for Nominal Transition Systems

## TL;DR

This paper introduces a general framework for nominal transition systems with a corresponding Hennessy-Milner logic, accommodating various bisimulation types and formalized in Nominal Isabelle, advancing the theoretical understanding of nominal process logics.

## Contribution

It defines a unified approach to nominal transition systems with a new logic, including technical innovations like infinite conjunctions, and systematically treats different bisimulation variants.

## Key findings

- Hennessy-Milner logic is adequate and complete for these systems.
- The framework supports various bisimulation types systematically.
- Main theorems are formalized in Nominal Isabelle.

## Abstract

We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.