Sciweavers

FORMATS
2007
Springer
14 years 4 months ago
Efficient On-the-Fly Algorithms for Partially Observable Timed Games
In this paper, we review some recent results on the efficient synthesis of controllers for timed systems. We first recall the basics of controller synthesis for timed games and the...
Franck Cassez
FORMATS
2007
Springer
14 years 4 months ago
Partial Order Reduction for Verification of Real-Time Components
Abstract. We describe a partial order reduction technique for a realtime component model. Components are described as timed automata with data ports, which can be composed in stati...
John Håkansson, Paul Pettersson
FORMATS
2007
Springer
14 years 4 months ago
CSL Model Checking Algorithms for Infinite-State Structured Markov Chains
Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov c...
Anne Remke, Boudewijn R. Haverkort
FORMATS
2007
Springer
14 years 4 months ago
Combining Formal Verification with Observed System Execution Behavior to Tune System Parameters
Resource limited DRE (Distributed Real-time Embedded) systems can benefit greatly from dynamic adaptation of system parameters. We propose a novel approach that employs iterative t...
Minyoung Kim, Mark-Oliver Stehr, Carolyn L. Talcot...
FORMATS
2007
Springer
14 years 4 months ago
Automatic Abstraction Refinement for Timed Automata
Henning Dierks, Sebastian Kupferschmid, Kim Guldst...
FORMATS
2007
Springer
14 years 6 months ago
Quantitative Model Checking Revisited: Neither Decidable Nor Approximable
Abstract. Quantitative model checking computes the probability values of a given property quantifying over all possible schedulers. It turns out that maximum and minimum probabilit...
Sergio Giro, Pedro R. D'Argenio
FORMATS
2007
Springer
14 years 6 months ago
Costs Are Expensive!
Patricia Bouyer, Nicolas Markey
FORMATS
2007
Springer
14 years 6 months ago
Hypervolume Approximation in Timed Automata Model Checking
Dierence Bound Matrices (DBMs) are the most commonly used data structure for model checking timed automata. Since long they are being used in successful tools like Kronos or UPPAA...
Víctor A. Braberman, Jorge Lucángeli...
FORMATS
2007
Springer
14 years 6 months ago
Counter-Free Input-Determined Timed Automata
We identify a class of timed automata, which we call counter-free input-determined automata, which characterize the class of timed languages definable by several timed temporal l...
Fabrice Chevalier, Deepak D'Souza, Pavithra Prabha...
FORMATS
2007
Springer
14 years 6 months ago
AMT: A Property-Based Monitoring Tool for Analog Systems
Abstract. In this paper we describe AMT, a tool for monitoring temporal properties of continuous signals. We first introduce STL/PSL, a specification formalism based on the indus...
Dejan Nickovic, Oded Maler