Temporal Logics on Words with Multiple Data Values

Ahmet Kara

Thursday, March 15th, 2013 at 10:30.

Polacksbacken, room 1145

We propose and study Data LTL, a temporal logic for attributed words, that is, words where every position carries some symbols from a finite alphabet and some data values from an infinite set. We consider a basic logic which is a semantical fragment of the logic Freeze LTL of Demri and Lazic with operators for navigation into the future and the past. By reduction to the emptiness problem for data automata it is shown that this basic logic is decidable. Whereas the basic logic only allows navigation along positions carrying the same data value, we study extensions that also allow navigation to positions with different data values. Finally, we discuss the applicability of Data LTL in the area of Model Checking of systems with unboundedly many processes.