On the verification of parametric and realtime systems

Description:tesi di dottoratoShow FileMIME type:application/pdfFile Size:2.9 Mb
tesi B. Di Giampaolo.pdf

Description:abstract in inglese a cura dell'autoreShow FileMIME type:application/pdfFile Size:294.0 Kb
abstract in inglese B. Di Giampaolo.pdf
Soggetto
Model checking; Synthesis; Temporal logicsAbstract
Parametric and RealTime Systems play a central role in the theory underlying
the Verification and Synthesis problems.
Realtime systems are present everywhere and are used in safety critical
applications, such as flight controllers. Failures in such systems can be
very expensive and even life threatening and, moreover, they are quite
hard to design and verify. For these reasons, the development of formal
methods for the modeling and analysis of safetycritical systems is
an active area of computer science research.
The standard formalism used to specify the wished behaviour of a realtime
system is temporal logic. Traditional temporal logics, such as linear
temporal logic (LTL), allow only qualitative assertions about the temporal
ordering of events. However, in several circumstances, for assessing the
efficiency of the system being modeled, it may be useful to have additional
quantitative guarantees. An extension of LTL with a realtime semantics
is given by the Metric Interval Temporal Logic (MITL), where changes
of truth values happen according to a splitting of the line of nonnegative
reals into intervals.
However, even with quantitative temporal logics, we would actually like
to find out what quantitative bounds can be placed on the logic operators.
In this thesis we face with the above problem proposing a parametric
extension of MITL, that is the parametric metric interval temporal logic
(PMITL), which allows to introduce parameters within intervals . For this
logic, we study decision problems which are the analogous of satisfiability,
validity and modelchecking problems for nonparametric temporal
logic. PMITL turns out to be decidable and we show that, when parameter
valuations give only nonsingular sets, the considered problems are all
decidable, EXPSPACEcomplete, and have the same complexity as in MITL.
Moreover, we investigate the computational complexity of these problems
for natural fragments of PMITL, and show that in meaningful fragments
of the logic they are PSPACEcomplete.
We also consider a remarkable problem expressed by queries where the
values that each parameter may assume are either existentially or universally
quantified. We solve this problem in several cases and we propose an
algorithm in EXPSPACE.
Another interesting application of the temporal logic is when it is used
to express specification of concurrent programs, where programs and properties
are formalized as regular languages of infinite words. In this case,
the verification problem (whether the program satisfies the specification)
corresponds to solve the language inclusion problem.
In the second part of this thesis we consider the Synthesis problem for realtime
systems, investigating the applicability of automata constructions that
avoid determinization for solving the language inclusion problem and the
realizability problem for realtime logics. Since Safra’s determinization
procedure is difficult to implement, we present Safraless algorithms for
automata on infinite timed words. [edited by author]
Descrizione
2009  2010
Collections
Data
20110506Autore
Di Giampaolo, Barbara
Metadata
Mostra tutti i dati dell'itemAutori  Di Giampaolo, Barbara  
Data Realizzazione  20111116T11:52:38Z  
Date Disponibilità  20111116T11:52:38Z  
Data di Pubblicazione  20110506  
Identificatore (URI)  http://hdl.handle.net/10556/188  
Descrizione  2009  2010  en_US 
Abstract  Parametric and RealTime Systems play a central role in the theory underlying the Verification and Synthesis problems. Realtime systems are present everywhere and are used in safety critical applications, such as flight controllers. Failures in such systems can be very expensive and even life threatening and, moreover, they are quite hard to design and verify. For these reasons, the development of formal methods for the modeling and analysis of safetycritical systems is an active area of computer science research. The standard formalism used to specify the wished behaviour of a realtime system is temporal logic. Traditional temporal logics, such as linear temporal logic (LTL), allow only qualitative assertions about the temporal ordering of events. However, in several circumstances, for assessing the efficiency of the system being modeled, it may be useful to have additional quantitative guarantees. An extension of LTL with a realtime semantics is given by the Metric Interval Temporal Logic (MITL), where changes of truth values happen according to a splitting of the line of nonnegative reals into intervals. However, even with quantitative temporal logics, we would actually like to find out what quantitative bounds can be placed on the logic operators. In this thesis we face with the above problem proposing a parametric extension of MITL, that is the parametric metric interval temporal logic (PMITL), which allows to introduce parameters within intervals . For this logic, we study decision problems which are the analogous of satisfiability, validity and modelchecking problems for nonparametric temporal logic. PMITL turns out to be decidable and we show that, when parameter valuations give only nonsingular sets, the considered problems are all decidable, EXPSPACEcomplete, and have the same complexity as in MITL. Moreover, we investigate the computational complexity of these problems for natural fragments of PMITL, and show that in meaningful fragments of the logic they are PSPACEcomplete. We also consider a remarkable problem expressed by queries where the values that each parameter may assume are either existentially or universally quantified. We solve this problem in several cases and we propose an algorithm in EXPSPACE. Another interesting application of the temporal logic is when it is used to express specification of concurrent programs, where programs and properties are formalized as regular languages of infinite words. In this case, the verification problem (whether the program satisfies the specification) corresponds to solve the language inclusion problem. In the second part of this thesis we consider the Synthesis problem for realtime systems, investigating the applicability of automata constructions that avoid determinization for solving the language inclusion problem and the realizability problem for realtime logics. Since Safra’s determinization procedure is difficult to implement, we present Safraless algorithms for automata on infinite timed words. [edited by author]  en_US 
Lingua  en  en_US 
Editore  Universita degli studi di Salerno  en_US 
Soggetto  Model checking  en_US 
Soggetto  Synthesis  en_US 
Soggetto  Temporal logics  en_US 
Titolo  On the verification of parametric and realtime systems  en_US 
Tipo  Doctoral Thesis  en_US 
MIUR  INF/01 INFORMATICA  en_US 
Coordinatore  Napoli, Margherita  en_US 
Ciclo  IX n.s.  en_US 
Tutor  Napoli, Margherita  en_US 
Dipartimento  Informatica  en_US 