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.
2006
Trento
Università degli Studi di Trento - Dipartimento di Informatica e Telecomunicazioni
A Decidable Extension of Hennessy-Milner Logic with Spatial Operators / Mardare, Radu; Priami, Corrado. - ELETTRONICO. - (2006), pp. 1-42.
Mardare, Radu; Priami, Corrado
File in questo prodotto:
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

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/357997
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
  • OpenAlex ND
social impact