|
|
 |
|
Mercredi 4 Mars
| Heure: |
09:30 - 10:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
On an Extension of Freeze LTL with Ordered Attributes |
| Description: |
Normann Decker We present an extension of Freeze LTL, a temporal logic equipped with registers,
over data words. Each position in a (multi-attributed) data word carries a
letter from a finite alphabet and assigns a data value to a fixed, finite set of
attributes. While reasoning on collections of data values is valuable for
expressing correctness properties of executions of dynamic programs the
satisfiability problem of Freeze LTL is undecidable if more than one register is
available or tuples of data values can be stored and compared arbitrarily. Our
extension therefore allows for specifying a dependency relation on attributes.
These dependencies introduce a restricted, yet flexible way of storing and
comparing collections of attribute values. This new dimension of flexibility is
orthogonal to, e.g., the number of registers or the available temporal
operators. In this setting we characterise precisely the type of dependency
relations that maintain decidability of the logic. To this end, we employ
reductions from and to nested counter systems. Moreover, by a complexity
theoretic characterisations we can show that our extension is strict and induces
a semantic hierarchy of logical fragments. |
|
|
