TY - GEN
T1 - Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory
AU - Beneš, Nikola
AU - Delahaye, Benoît
AU - Fahrenberg, Uli
AU - Křetínský, Jan
AU - Legay, Axel
PY - 2013
Y1 - 2013
N2 - There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers.
AB - There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers.
UR - http://www.scopus.com/inward/record.url?scp=84882788355&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40184-8_7
DO - 10.1007/978-3-642-40184-8_7
M3 - Conference contribution
AN - SCOPUS:84882788355
SN - 9783642401831
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 76
EP - 90
BT - Concurrency Theory - 24th International Conference, CONCUR 2013, Proceedings
T2 - 24th International Conference on Concurrency Theory, CONCUR 2013
Y2 - 27 August 2013 through 30 August 2013
ER -