Linear parametric model checking of timed automata

Autor: Thomas Hune, Frits W. Vaandrager, Mariëlle Stoelinga, Judi Romijn

Publikováno v: Journal of Logic and Algebraic Programming, 52-53, 183-220. Elsevier
Journal of Logic and Algebraic Programming, 52-53, pp. 183-220
Journal of Logic and Algebraic Programming, 52-53, 183-220
BRICS Report Series; No 5 (2001): RS-5 Linear Parametric Model Checking of Timed Automata
BRICS Report Series; Nr. 5 (2001): RS-5 Linear Parametric Model Checking of Timed Automata

We present an extension of the model checker Uppaal capable of synthesizing linear parameter constraints for the correctness ofparametric timed automata. The symbolic representation of the (parametric) state-space is shown to be correct. A second con

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6dc2b534ca151141c7fff75fbb0bb8fc
https://research.tue.nl/nl/publications/2a7a5a23-9f67-4980-ac58-645635dabbc3

Guided Synthesis of Control Programs for a Batch Plant using UPPAAL

Autor: Paul Pettersson, Kim Guldstrand Larsen, Thomas Hune

Publikováno v: BRICS Report Series; No 37 (2000): RS-37 Guided Synthesis of Control Programs for a Batch Plant using UPPAAL
BRICS Report Series; Nr. 37 (2000): RS-37 Guided Synthesis of Control Programs for a Batch Plant using UPPAAL

In this paper we address the problem of scheduling and synthesizing distributed control programs for a batch production plant. We use a timed automata model of the batch plant and the verification tool Uppaal to solve the scheduling problem.In modeli

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6ad32969734f678285d0e8ea703df54d
https://doi.org/10.7146/brics.v7i37.20203

Modeling a Language for Embedded Systems in Timed Automata

Autor: Thomas Hune

Publikováno v: BRICS Report Series; No 17 (2000): RS-17 Modeling a Language for Embedded Systems in Timed Automata
BRICS Report Series; Nr. 17 (2000): RS-17 Modeling a Language for Embedded Systems in Timed Automata

We present a compositional method for translating real-timeprograms into networks of timed automata. Programs are written in anassembly like real-time language and translated into models supportedby the tool Uppaal. We have implemented the translatio

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5a1054b0f88fa2d4877380b88daa7b7b
https://doi.org/10.7146/brics.v7i17.20144

A Case Study on Using Automata in Control Synthesis

Autor: Thomas Hune, Anders B. Sandholm

Publikováno v: Fundamental Approaches to Software Engineering ISBN: 9783540672616
FASE

We study a method for synthesizing control programs. The method merges an existing control program with a control automaton. We have used monadic second order logic over strings to specify the control automata. Specifications are translated into auto

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::4060ed1d074837a9db340cc5d26d30b8
https://doi.org/10.1007/3-540-46428-x_24

Timed bisimulation and open maps

Autor: Thomas Hune, Mogens Nielsen

Publikováno v: Mathematical Foundations of Computer Science 1998 ISBN: 9783540648277
MFCS

Open maps have been used for defining bisimulations for a range of models, but none of these have modelled real-time. We define a category of timed transition systems, and use the general framework of open maps to obtain a notion of bisimulation. We

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::c7cf03bcf71573310c3b07acdddd2906
https://doi.org/10.1007/bfb0055787