Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BENEŠ Nikola DELAHAYE Benoit FAHRENBERG Uli KŘETÍNSKÝ Jan LEGAY Axel

Rok publikování 2013
Druh Článek ve sborníku
Konference CONCUR 2013 - Concurrency Theory - 24th International Conference
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-40184-8_7
Obor Informatika
Klíčová slova modal transition systems; composition; specification; interface theory
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info