In this paper we focus on Dynamic Spatial Logic, the extension of Hennessy-Milner logic with the parallel operator. We develop a sound complete Hilbert-style axiomatic system for it comprehending the behavior of spatial operators in relation with dynamic/temporal ones. Underpining on a new congruence we define over the class of processes - the structural bisimulation - we prove the finite model property for this logic that provides the decidability for satisfiability, validity and model checking against process semantics.
A Decidable Extension of Hennessy-Milner Logic with Spatial Operators / Mardare, Radu; Priami, Corrado. - ELETTRONICO. - (2006), pp. 1-42.
A Decidable Extension of Hennessy-Milner Logic with Spatial Operators
Mardare, Radu;Priami, Corrado
2006-01-01
Abstract
In this paper we focus on Dynamic Spatial Logic, the extension of Hennessy-Milner logic with the parallel operator. We develop a sound complete Hilbert-style axiomatic system for it comprehending the behavior of spatial operators in relation with dynamic/temporal ones. Underpining on a new congruence we define over the class of processes - the structural bisimulation - we prove the finite model property for this logic that provides the decidability for satisfiability, validity and model checking against process semantics.File | Dimensione | Formato | |
---|---|---|---|
DIT-06-009.pdf
accesso aperto
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
2.15 MB
Formato
Adobe PDF
|
2.15 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione