2018/12/04 by Ulrich Dorsch, Dorsch, Ulrich, Stefan Milius +3
Computer Science · #03B45 #03B70 #18C10 #18C15 #18C20 #Category Theory (math.CT) #F.1.2 #F.3.1 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1812.01317
openalex publication_date 2018/12/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
State-based models of concurrent systems are traditionally considered under a\nvariety of notions of process equivalence. In the particular case of labelled\ntransition systems, these equivalences range from trace equivalence to (strong)\nbisimilarity, and are organized in what is known as the linear time --\nbranching time spectrum. A combination of universal coalgebra and graded monads\nprovides a generic framework in which the semantics of concurrency can be\nparametrized both over the branching type of the underlying transition systems\nand over the granularity of process equivalence. We show in the present paper\nthat this framework of graded semantics does subsume the most important\nequivalences from the linear time -- branching time spectrum. An important\nfeature of graded semantics is that it allows for the principled extraction of\ncharacteristic modal logics. We have established invariance of these graded\nlogics under the given graded semantics in earlier work; in the present paper,\nwe extend the logical framework with an explicit propositional layer and\nprovide a generic expressiveness criterion that generalizes the classical\nHennessy-Milner theorem to coarser notions of process equivalence. We extract\ngraded logics for a range of graded semantics on labelled transition systems\nand probabilistic systems, and give exemplaric proofs of their expressiveness\nbased on our generic criterion.\n