This manuscript is a revised version of the PhD Thesis I wrote under the supervision of Prof. Angelo Montanari at Udine University. The leitmotif underlying the results herein provided is that, given any infinite complex system (e.g., a computer program) to be verified against a finite set of properties, there often exists a simpler system that satisfies the same properties and, in addition, presents strong regularities (e.g., periodicity) in its structure. Those regularities can then be exploited to decide, in an effective way, which property is satisfied by the system and which is not. Perhaps the most natural and effective way to deal with inherent regularities of infinite systems is through the notion of finitestate automaton. Intuitively, a finitestate automaton is an abstract machine with only a bounded amount of memory at its disposal, which processes an input (e.g., a sequence of symbols) and eventually outputs true or false, depending on the way the machine was designed and on the input itself. The present book focuses precisely on automatonbased approaches that ease the representation of and the reasoning on properties of infinite complex systems. The most simple notion of finitestate automaton, is that of singlestring automaton. Such a device outputs true on a single (finite or infinite) sequence of symbols and false on any other sequence. We will show how singlestring automata processing infinite sequences of symbols can be successfully applied in various frameworks for temporal representation and reasoning. In particular, we will use them to model single ultimately periodic time granularities, namely, temporal structures that are leftbounded and that, ultimately, periodically group instants of the underlying temporal domain (a simple example of such a structure is given by the partitioning of the temporal domain of days into weeks). The notion of singlestring automaton can be further refined by introducing counters in order to compactly represent repeated occurrences of the same subsequence in the given input. By introducing restricted policies of counter update and by exploiting suitable abstractions of the configuration space for the resulting class of automata, we will devise efficient algorithms for reasoning on quasiperiodic time granularities (e.g., the partitioning of the temporal domain of days into years). Similar abstractions can be used when reasoning on infinite branching (temporal) structures. In such a case, one has to consider a generalized notion of automaton, which is able to process labeled branching structures (hereafter called trees), rather than linear sequences of symbols. We will show that sets of trees featuring the same properties can be identified with the equivalence classes induced by a suitable automaton. More precisely, given a property to be verified, one can first define a corresponding automaton that accepts all and only the trees satisfying that property, then introduce a suitable equivalence relation that refines the standard language equivalence and groups all trees being indistinguishable by the automaton, and, finally, exploit such an equivalence to reduce several instances of the verification problem to equivalent simpler instances, which can be eventually decided.
Automata for branching and layered temporal structures: An investigation into regularities of infinite transition systems
Puppis G.^{}
20100101
Abstract
This manuscript is a revised version of the PhD Thesis I wrote under the supervision of Prof. Angelo Montanari at Udine University. The leitmotif underlying the results herein provided is that, given any infinite complex system (e.g., a computer program) to be verified against a finite set of properties, there often exists a simpler system that satisfies the same properties and, in addition, presents strong regularities (e.g., periodicity) in its structure. Those regularities can then be exploited to decide, in an effective way, which property is satisfied by the system and which is not. Perhaps the most natural and effective way to deal with inherent regularities of infinite systems is through the notion of finitestate automaton. Intuitively, a finitestate automaton is an abstract machine with only a bounded amount of memory at its disposal, which processes an input (e.g., a sequence of symbols) and eventually outputs true or false, depending on the way the machine was designed and on the input itself. The present book focuses precisely on automatonbased approaches that ease the representation of and the reasoning on properties of infinite complex systems. The most simple notion of finitestate automaton, is that of singlestring automaton. Such a device outputs true on a single (finite or infinite) sequence of symbols and false on any other sequence. We will show how singlestring automata processing infinite sequences of symbols can be successfully applied in various frameworks for temporal representation and reasoning. In particular, we will use them to model single ultimately periodic time granularities, namely, temporal structures that are leftbounded and that, ultimately, periodically group instants of the underlying temporal domain (a simple example of such a structure is given by the partitioning of the temporal domain of days into weeks). The notion of singlestring automaton can be further refined by introducing counters in order to compactly represent repeated occurrences of the same subsequence in the given input. By introducing restricted policies of counter update and by exploiting suitable abstractions of the configuration space for the resulting class of automata, we will devise efficient algorithms for reasoning on quasiperiodic time granularities (e.g., the partitioning of the temporal domain of days into years). Similar abstractions can be used when reasoning on infinite branching (temporal) structures. In such a case, one has to consider a generalized notion of automaton, which is able to process labeled branching structures (hereafter called trees), rather than linear sequences of symbols. We will show that sets of trees featuring the same properties can be identified with the equivalence classes induced by a suitable automaton. More precisely, given a property to be verified, one can first define a corresponding automaton that accepts all and only the trees satisfying that property, then introduce a suitable equivalence relation that refines the standard language equivalence and groups all trees being indistinguishable by the automaton, and, finally, exploit such an equivalence to reduce several instances of the verification problem to equivalent simpler instances, which can be eventually decided.File  Dimensione  Formato  

FoLLILNAIMonograph2010.pdf
non disponibili
Tipologia:
Documento in Preprint
Licenza:
Non pubblico
Dimensione
2.7 MB
Formato
Adobe PDF

2.7 MB  Adobe PDF  Visualizza/Apri Richiedi una copia 
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.