2013/06/04 by Nikola Beneš, Benoît Delahaye, Beneš, Nikola +7
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Natural Language Processing Techniques #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1306.0741
openalex publication_date 2013/06/04 · openalex created_date 2022/09/16 · openalex updated_date 2026/07/28
There are two fundamentally different approaches to specifying and verifying\nproperties of systems. The logical approach makes use of specifications given\nas formulae of temporal or modal logics and relies on efficient model checking\nalgorithms; the behavioural approach exploits various equivalence or refinement\nchecking methods, provided the specifications are given in the same formalism\nas implementations.\n In this paper we provide translations between the logical formalism of\nHennessy-Milner logic with greatest fixed points and the behavioural formalism\nof disjunctive modal transition systems. We also introduce a new operation of\nquotient for the above equivalent formalisms, which is adjoint to structural\ncomposition and allows synthesis of missing specifications from partial\nimplementations. This is a substantial generalisation of the quotient for\ndeterministic modal transition systems defined in earlier papers.\n