Model construction for implicit specifications in modal logic

Autor:	Jarl Tuxen Lang, Kim Guldstrand Larsen, Christian Jeppesen, Ole Høgh Jensen
Rok vydání:	1993
Předmět:	Recursion Computer science Programming language Process calculus Of the form Context (language use) computer.software_genre computer Reactive system
Zdroj:	CONCUR'93 ISBN: 9783540572084 CONCUR
DOI:	10.1007/3-540-57208-2_18
Popis:	In top-down design of reactive systems, implicit specifications of the form C(P1, ..., Pn) sat F are often encountered, where C(P1, ..., Pn) is a system containing the (unknown) processes P1, ..., Pn, and F is a specification. We present a method for constructing the processes P1, ..., Pn (as labelled transition systems) when C is given as a context of process algebra (such as CCS), and F is given as a formula of Hennessy-Milner Logic extended with maximal recursion. The main contribution is the treatment of the simultaneous construction of several processes which together act as a model for the specification. We have implemented two prototype tools (a semi-automatic as well as an automatic one) which are based on the presented theory.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::43efdb7e3e80875f4ade8827cf58a7ac https://doi.org/10.1007/3-540-57208-2_18 Zobrazit plný text záznamu