PhD defence by Line Juhl

In partial fulfillment of the terms for obtaining the Ph.D. degree, Line Juhl will give a lecture on the following subject:

Quantities in Games and Modal Transition Systems

on Monday 14th of May 2012, 13.00,
in room 02.12 at Selma Lagerlöfs Vej 300

Abstract:
As embedded software becomes an increasing part of our daily lives, modelling and verification of embedded systems is highly relevant. Common for many embedded software systems is the restricted use of and access to resources. Thus modelling and verification of embedded systems must not only rely on functional requirements, but also extra-functional requirements such as fuel consumption or bandwidth usage. This thesis presents formalisms for modelling such quantitative systems and focuses on both the inherent reactive characteristic of embedded systems, implied by the surrounding environment, as well as on the need for compositional reasoning.

In order to develop applicable formalisms, the challenges of embedded systems are discussed in order to identify useful methods and theories for dealing with the quantitative aspects of reactive systems. This includes game theory for modelling the reactive aspects and modal transition systems as the basis for a compositional specification theory allowing a stepwise refinement. Related to game theory we investigate the recently emerged notion of energy games, where we study the existence of infinite runs in multiweighed games subject to boundary constraints on the accumulated weights. We give tight complexity bounds for deciding the problem in a number of different settings and show undecidability in two other cases. In the case of unknown upper bounds we provide a method for constructing the exact set of upper bounds yielding such infinite runs.

For compositional reasoning we define and study weighted modal transition systems and two extensions to a multiweighed setting. The first extension allows for refinable labels and we prove that the key notions behave as expected. The second extension presents a logic for reasoning on the accumulated weight along the runs. The semantics of the logic is game-based and is thereby proven to be both sound and complete. The logic is proven undecidable in general; however useful decidable fragments are identified.

Members of the assessment committee are Professor Antonín Kučera, Masaryk University, Brno, Czech Republic, Professor Peter Bro Miltersen, Aarhus University, Denmark, and Associate Professor René Rydhof Hansen, Aalborg University, Denmark. Professor Kim G. Larsen and Associate Professor Jiří Srba are Line Juhl’s supervisors. Moderator associate professor Brian Nielsen.

All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.