Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1112166, author = {Beneš, Nikola and Delahaye, Benoit and Fahrenberg, Uli and Křetínský, Jan and Legay, Axel}, address = {Heidelberg Dordrecht London New York}, booktitle = {CONCUR 2013 - Concurrency Theory - 24th International Conference}, doi = {http://dx.doi.org/10.1007/978-3-642-40184-8_7}, keywords = {modal transition systems; composition; specification; interface theory}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Heidelberg Dordrecht London New York}, isbn = {978-3-642-40183-1}, pages = {76-90}, publisher = {Springer}, title = {Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory}, year = {2013} }
TY - JOUR ID - 1112166 AU - Beneš, Nikola - Delahaye, Benoit - Fahrenberg, Uli - Křetínský, Jan - Legay, Axel PY - 2013 TI - Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory PB - Springer CY - Heidelberg Dordrecht London New York SN - 9783642401831 KW - modal transition systems KW - composition KW - specification KW - interface theory 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. ER -
BENEŠ, Nikola, Benoit DELAHAYE, Uli FAHRENBERG, Jan KŘETÍNSKÝ a Axel LEGAY. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. In \textit{CONCUR 2013 - Concurrency Theory - 24th International Conference}. Heidelberg Dordrecht London New York: Springer, 2013, s.~76-90. ISBN~978-3-642-40183-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-40184-8\_{}7.
|