### Abstract

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.

### License

BSD License

### History

January 29, 2017
  Formalization of weak bisimilarity added (revision c87cc2057d9c)

### Topics

- Computer science/Concurrency/Process calculi
- Logic/General logic/Modal logic

### Session Modal_Logics_for_NTS

- Nominal_Bounded_Set
- Nominal_Wellfounded
- Residual
- Transition_System
- Formula
- Validity
- Logical_Equivalence
- Bisimilarity_Implies_Equivalence
- Equivalence_Implies_Bisimilarity
- Disjunction
- Expressive_Completeness
- FS_Set
- FL_Transition_System
- FL_Formula
- FL_Validity
- FL_Logical_Equivalence
- FL_Bisimilarity_Implies_Equivalence
- FL_Equivalence_Implies_Bisimilarity
- L_Transform
- Weak_Transition_System
- Weak_Formula
- Weak_Validity
- Weak_Logical_Equivalence
- Weak_Bisimilarity_Implies_Equivalence
- Weak_Equivalence_Implies_Bisimilarity
- Weak_Expressive_Completeness
- S_Transform

### Depends on

- Nominal 2

## Cite

×

Modal_Logics_for_NTS-AFP

    @article{Modal_Logics_for_NTS-AFP,
      author  = {Tjark Weber and Lars-Henrik Eriksson and Joachim Parrow and Johannes Borgström and Ramunas Gutkovas},
      title   = {Modal Logics for Nominal Transition Systems},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Modal_Logics_for_NTS.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Oct 27, 2016 : Isabelle2016
- Oct 25, 2016 : Isabelle2016