2017/04/24 by Marino Miculan, Marco Peressotti, Miculan, Marino +1
Computer Science · #Advanced Database Systems and Queries #F.1.2 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1704.07181
openalex publication_date 2017/04/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Weighted labelled transition systems (WLTSs) are an established meta-model\naiming to provide general results and tools for a wide range of systems such as\nnon-deterministic, stochastic, and probabilistic systems. In order to encompass\nprocesses combining several quantitative aspects, extensions of the WLTS\nframework have been further proposed, state-to-function transition systems\n(FuTSs) and uniform labelled transition systems (ULTraSs) being two prominent\nexamples. In this paper we show that this hierarchy of meta-models collapses\nwhen studied under the lens of bisimulation-coherent encodings. Taking\nadvantage of these reductions, we derive a fully abstract Hennessy-Milner-style\nlogic for FuTSs, i.e., which characterizes quantitative bisimilarity, from a\nfully-abstract logic for WLTSs.\n