The Symmetry of the Past and of the Future: Bi-infinite Time in the Verification of Temporal Properties (Contributo in atti di convegno)

Type

• Contributo in atti di convegno (Classe)
• Prodotto della ricerca (Classe)

Label

• The Symmetry of the Past and of the Future: Bi-infinite Time in the Verification of Temporal Properties (Contributo in atti di convegno) (literal)

Anno

• 2007-01-01T00:00:00+01:00 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi

• 10.1145/1287624.1287669 (literal)

Alternative label

• M. Pradella, A. Morzenti, P. San Pietro (2007)
  The Symmetry of the Past and of the Future: Bi-infinite Time in the Verification of Temporal Properties
  in 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007), Dubrovnik, Croatia, 2007
  (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori

• M. Pradella, A. Morzenti, P. San Pietro (literal)

Pagina inizio

• 312 (literal)

Pagina fine

• 320 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#titoloVolume

• ESEC-FSE '07 Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering (literal)

Note

• Scopus (literal)
• Google Scholar (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni

• Politecnico di Milano (literal)

Titolo

• The Symmetry of the Past and of the Future: Bi-infinite Time in the Verification of Temporal Properties (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn

• 978-1-59593-811-4 (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#curatoriVolume

• Ivica Crnkovic (literal)

Abstract

• Model checking techniques have traditionally dealt with temporal logic languages and automata interpreted over ?-words, i.e., infi- nite in the future but finite in the past. However, time with also an infinite past is a useful abstraction in specification. It allows one to ignore the complexity of system initialization in much the same way as system termination may be abstracted away by allowing an infinite future. One can then write specifications that are simpler and more easily understandable, because they do not include the description of the operations (such as configuration or installation) typically performed at system deployment time. The present pa- per is centered on the problem of satisfiability checking of linear temporal logic (LTL) formulae with past operators. We show that bounded model checking techniques can be adapted to deal with bi-infinite time in temporal logic, without incurring in any perfor- mance loss. Our claims are supported by a tool, whose application to a case study shows that satisfiability checking may be feasible also on nontrivial examples of temporal logic specifications. (literal)

Editore

• ACM Press (Editore)

Prodotto di

• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)
• Istituto di elettronica e di ingegneria dell'informazione e delle telecomunicazioni (IEIIT) (Istituto)

Autore CNR

• MATTEO PRADELLA (Unità di personale interno)

Incoming links:

Prodotto

• Istituto di elettronica e di ingegneria dell'informazione e delle telecomunicazioni (IEIIT) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

Autore CNR di

• MATTEO PRADELLA (Unità di personale interno)

Editore di

• ACM Press (Editore)