Dies sind die archivierten Webseiten des Lehrstuhls für Programmierung und Softwaretechnik (PST).
Die Seiten des Software and Computational Systems Lab (SoSy) finden Sie auf https://www.sosy-lab.org/.

Startseite > Lehre > Oberseminar > Sommersemester 2012 > Oberseminar 28.08.12

Oberseminar 28.08.12

— abgelegt unter:

Wissenschaftlicher Vortrag: Mikael H. Møller

Was
  • Oberseminar
Wann 28.08.2012
von 14:15 bis 15:45
Wo Raum 061, Oettingenstr. 67
Termin übernehmen vCal
iCal

Einladung zum

Oberseminar Methoden und Theorie der Software-Entwicklung

======================================

Datum und Zeit: Dienstag, 28. August 2012 - 14:15 Uhr

Raum: 061, Oettingenstraße 67

Es spricht: Mikael H. Møller

Über: Extended Modal Transisiton Systems

 

Modal transition systems (MTS) is a well-studied specification formalism of  reactive systems supporting a step-wise refinement methodology.Despite its many advantages, the formalism as well as its currentlyknown extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices.We have introduced a new model called parametric modal transition systems (PMTS)together with a general modal refinement notion that overcome many of the limitations and we investigate the computational complexity of modal refinement checking. 

Secondly we have exteded the modal specifications with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.
 
Finally we define a logic for Boolean MTS (BMTS), and present the characteristic formula for such specification, using a version of HML with recursion. We prove that our logic characterizes the modal refinement of BMTS. Further we apply our logic on the more general PMTS, where we show how to select the parameters of a PMTS, under certain requirements expressed in the logic.
iCalendar vCalendar Drucken
nach oben
Impressum - Datenschutz Kontakt