Behavioural Preorders via Graded Monads
Ford M, Milius S, Schröder L (2021)
Publication Language: English
Publication Type: Conference contribution
Publication year: 2021
Journal
Publisher: Institute of Electrical and Electronics Engineers Inc.
City/Town: New York, NY, United States
Book Volume: 2021-June
Pages Range: 1--13
Conference Proceedings Title: Proceedings - Symposium on Logic in Computer Science
Event location: Rome, Italy (Online)
ISBN: 9781665448956
DOI: 10.1109/LICS52264.2021.9470517
Abstract
Like notions of process equivalence, behavioural preorders on processes come in many flavours, ranging from fine-grained comparisons such as ready simulation to coarse-grained ones such as trace inclusion. Often, such behavioural preorders are characterized in terms of theory inclusion in dedicated characteristic logics; e.g. simulation is characterized by theory inclusion in the positive fragment of Hennessy-Milner logic. We introduce a unified semantic framework for behavioural preorders and their characteristic logics in which we parametrize the system type as a functor on the category Pos of partially ordered sets following the paradigm of universal coalgebra, while behavioural preorders are captured as graded monads on Pos, in generalization of a previous approach to notions of process equivalence. We show that graded monads on Pos are induced by a form of graded inequational theories that we introduce here. Moreover, we provide a general notion of modal logic compatible with a given graded behavioural preorder, along with a criterion for expressiveness, in the indicated sense of characterization of the behavioural preorder by theory inclusion. We illustrate our main result on various behavioural preorders on labelled transition systems and probabilistic transition systems.
Authors with CRIS profile
Matthew Ford
Graduiertenkolleg 2475 Cyberkriminalität und Forensische Informatik
Stefan Milius
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Lutz Schröder
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Related research project(s)
How to cite
APA:
Ford, M., Milius, S., & Schröder, L. (2021). Behavioural Preorders via Graded Monads. In Proceedings - Symposium on Logic in Computer Science (pp. 1--13). Rome, Italy (Online), IT: New York, NY, United States: Institute of Electrical and Electronics Engineers Inc..
MLA:
Ford, Matthew, Stefan Milius, and Lutz Schröder. "Behavioural Preorders via Graded Monads." Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy (Online) New York, NY, United States: Institute of Electrical and Electronics Engineers Inc., 2021. 1--13.
BibTeX: Download