Towards a mobile temporal logic of actions [Elektronische Ressource] / vorgelegt von Júlia Zappe

Júlia Zappe

Sujets

• Informatik

Informations

• Publié par: ludwig-maximilians-universitat_munchen
• Publié le: 01 janvier 2005
• Nombre de lectures: 9
• Langue: English

Extrait

Towards a Mobile Temporal Logic of Actions
Julia´ Zappe
Dissertation an der Fakultat¨ fur¨ Mathematik, Informatik und Statistik der
Ludwig Maximilians Universit at¨ Munchen¨
vorgelegt von Julia´ Zappe
Munchen,¨ den 8.7.2005ii
Erstgutachter: Prof. Dr. Fred Kroger¨
Zweitgutachter: Dr. Stephan Merz
Externer Gutachter: Prof. Dr. Holger Schlingloff
Tag der mundlichen¨ Prufung:¨ 22.9.2005iii
Acknowledgements
I would like to thank my supervisor Fred Kroger¨ . He was willing to discuss at
any time, and I could always rely on his full support. I am also thankful to him
for his encouragement, especially in some of the rather dragging phases of my
work. I am particularly grateful to Stephan Merz. Without his constant support
and admirable patience throughout the whole period of writing I probably would
not have been able to finish this thesis. I have not only benefited from his extraor-
dinary professional competence, but have also taken advantage of his exceptional
human qualities. I also would like to express my gratitude towards Martin Wirs
ing for providing me with a pleasant working environment by taking me into his
group. He always has shown much interest in my work. The idea for the subject
of this thesis was initiated by him and Stephan Merz.
I feel a need to thank all my friends and my family for not leaving me alone, not
even in times when I tended to be almost unbearable... I am aware that I have
demanded much of you by asking to share the burden with me. Thank you for not
running away!Contents
1 Introduction 3
2 Mobile TLA 7
2.1 The Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Example of a Mobile Agent . . . . . . . . . . . . . . . . . . . . . 10
2.3 Simple MTLA . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.4 Temporal stuttering . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.5 Spatial stuttering . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3 Refinement 29
3.1 Operation refinement . . . . . . . . . . . . . . . . . . . . . . . . 30
3.2 Spatial extension . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.2.1 Spatial extension without distribution of variables . . . . . 33
3.2.2 Spatial extension with distribution of variables . . . . . . 35
3.3 Virtualisation of locations . . . . . . . . . . . . . . . . . . . . . . 37
4 Axiomatisation 45
4.1 The proof system . . . . . . . . . . . . . . . . . . . . . . . . 46SL
v
Svi Contents
4.2 Axiomatisation of propositional MLTL . . . . . . . . . . . . . . . 62
4.2.1 The proof system . . . . . . . . . . . . . . . . . 62MLTL
4.2.2 The proof system . . . . . . . . . . . . . . . . . . 74MLTL
5 Model Checking & Decidability 85
5.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
5.2 Buchi¨ automata . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
5.3 Alternating Automata on Infinite Words . . . . . . . . . . . . . . 88
5.4 Automaton for propositional MLTL . . . . . . . . . . 103
5.5 Applications to decision problems . . . . . . . . . . . . . . . . . 107
6 Extensions of MTLA 111
6.1 Dynamic creation ofk agents . . . . . . . . . . . . . . . . . . . . 111
6.2 Dynamic creation of arbitrarily many agents . . . . . . . . . . . . 117
6.3 Rigid quantification over names . . . . . . . . . . . . . . . . . . 118
6.4 Hiding of anonymous agents . . . . . . . . . . . . . . . . . . . . 122
7 Conclusion 125
A Auxiliary derivations 127
Bibliography 133
SSContents 1
Zusammenfassung
Die vorliegende Arbeit stellt einen neuen Ansatz zur Spezifikation von mobilen
Systemen vor. Als mobiles System wird hier ein System bezeichnet, das Code
verwendet, der zur Laufzeit von einem Rechner auf einen anderen ubertragen¨
werden kann, und dessen Ausfuhrung¨ auf dem neuen Rechner fortgesetzt wird.
Ein solches System wird gern als eine Hierarchie von “Orten” modelliert, deren
Struktur verandert¨ werden kann. Dies ist auch der Ausgangspunkt fur¨ unseren
Modellbegriff. Es wird eine raum zeitliche Logik namens MTLA eingefuhrt,¨
deren temporaler Teil auf Lamports Temporal Logic of Actions (TLA) basiert.
Zusatzlich¨ werden raumliche¨ Modalitaten¨ definiert um die Struktur des Systems
und ihre Veranderungen¨ zu beschreiben. Geeignete Begriffe fur¨ die Verfeinerung
solcher Systeme sowie ihre Reprasentierbark¨ eit in MTLA werden untersucht. Des
weiteren wird den theoretischen Fragen der Axiomatisierbarkeit, der Erfullbark¨ eit
und des Model Checking Problems nachgegangen.
Abstract
In this thesis we present a novel approach to the specification of mobile systems.
By mobile system we mean a system that makes use of code that can be transmit
ted from one computer to another one at runtime, so that the execution is continued
on the new. Such systems are often modelled as a hierarchy of locations
whose structure can be modified. This is also the starting point for our model no
tion. We introduce a spatio temporal logic called MTLA whose temporal part is
based on Lamport’s Temporal Logic of Actions (TLA). In addition to the temporal
operators we define spatial modalities to describe the structure of the system and
its modifications. We study suitable notions for the refinement of such systems
as well as their representability in MTLA. Furthermore, we investigate theoretical
questions like axiomatisability, satisfiability and the model checking problem.Chapter 1
Introduction
With the lightning progress of networking technology and the increasing use of
networks the role of systems that make use of mobile code – the term “mobile
code” signifying code that can be transmitted to remote sites, even during execu
tion – becomes more and more important. As a particular kind of mobile systems,
mobile agent systems have arisen starting from the nineties [5, 8, 53]. A mobile
agent is a sort of mobile code with some specific properties. Simultaneously with
the development of such mobile systems, formal methods have been investigated
to support their design. In the course of these studies it has soon become clear
that traditional models of distributed systems are not adequate to capture certain
aspects of mobility.
The first formalism handling mobility that has gained wide attention and has
achieved recognition is Milner’s calculus [38]. The calculus extends the pro
cess algebra Calculus of Communicating Systems (CCS) [37] following an ap
proach proposed by Engberg and Nielsen [17]. The main characteristic of the -
calculus is that names of communication channels can be transmitted as messages.
This feature allows to express the modification of the communication structure of
the system.
As Cardelli has pointed out in [9], the calculus provides a good model to de
scribe mobility of distributed systems as long as only small, local area networks
are concerned. However, in the context of wide area networks mobility itself is not
3
pppp4
the only issue that has to be taken into account. In contrast to local area networks,
mutually distrustful administrative domains separated by barriers play a promi
nent role in the Internet. In order to adequately model mobility in large scale
networks, the crossing of boundaries between such protected domains by mobile
code should be explicitely expressible. Following this observation, several novel
formalisms (e.g. [11, 19, 15, 52]), mainly process calculi, have been introduced,
many of them based upon the calculus. A common feature of these formalisms
is the assumption that mobile systems have a hierarchical structure, and mobility
is modelled by allowing to modify this structure.
One of the best known of these calculi – and the one that has strongly influenced
and motivated our work – is the Ambient Calculus [11] by Cardelli and Gordon.
The Ambient Calculus is a process calculus where processes may reside at nodes
of an edge labelled tree. By executing some capabilities, the processes can modify
the tree structure. The basic primitives of the Ambient Calculus are similar to
those of the calculus.
For some of the above mentioned calculi modal logics have been introduced [10,
7, 16] to express properties of mobile systems. The models of these logics are the
process terms of the respective calculi. Beside temporal modalities they addition
ally use spatial modalities to describe modifications of the hierarchical structure
of the system. Typically, the formulas of these logics closely reflect the syntactic
structure of the process terms. In particular, they can separate terms that only dif
fer in their structure but have the same behaviour (with respect to the operational
semantics), in other words, process terms with the same behaviour can satisfy dif
ferent sets of formulas (cf. [47]). As a consequence, these logics do not seem to
be suitable as specification logics.
In the present thesis we suggest a different approach to specify mobile systems.
We propose a spatio temporal logic whose semantics is based onruns of mobile
systems, instead of a specific process calculus. In our approach – in imitation of
most of the mentioned calculi – such a run is (essentially) a sequence of finite
trees representing the topological structure of the system. However, there is a
local state at every node of the tree instead of a proc