Sciweavers

FORMATS
2008
Springer
14 years 8 days ago
MTL with Bounded Variability: Decidability and Complexity
This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the ...
Carlo A. Furia, Matteo Rossi
FORMATS
2008
Springer
14 years 8 days ago
Convergence Verification: From Shared Memory to Partially Synchronous Systems
Verification of partially synchronous distributed systems is difficult because of inherent concurrency and the potentially large state space of the channels. This paper identifies ...
K. Mani Chandy, Sayan Mitra, Concetta Pilotto
FORMATS
2008
Springer
14 years 8 days ago
Formal Modeling and Scheduling of Datapaths of Digital Document Printers
Abstract. We apply three different modeling frameworks -- timed automata (Uppaal), colored Petri nets and synchronous data flow -- to model a challenging industrial case study that...
Georgeta Igna, Venkatesh Kannan, Yang Yang, Twan B...
FORMATS
2008
Springer
14 years 8 days ago
Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities
The common metric temporal logics for continuous time were shown to be insufficient, when it was proved in [7, 12] that they cannot express a modality suggested by Pnueli. Moreover...
Alexander Rabinovich
FORMATS
2008
Springer
14 years 8 days ago
Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets
Time dependant models have been intensively studied for many reasons, among others because of their applications in software verification and due to the development of embedded pla...
Jirí Srba
FORMATS
2008
Springer
14 years 8 days ago
Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets
Abstract. We introduce and study hybrid automata with strong resets. They generalize o-minimal hybrid automata, a class of hybrid automata which allows modeling of complex continuo...
Patricia Bouyer, Thomas Brihaye, Marcin Jurdzinski...
FORMATS
2008
Springer
14 years 8 days ago
Infinite Runs in Weighted Timed Automata with Energy Constraints
We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the...
Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand...
FORMATS
2008
Springer
14 years 8 days ago
Some Recent Results in Metric Temporal Logic
Metric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we survey results about the complexity of the satisfiability and model c...
Joël Ouaknine, James Worrell
FORMATS
2008
Springer
14 years 8 days ago
On Scheduling Policies for Streams of Structured Jobs
We study a class of scheduling problems which combines the structural aspects associated with task dependencies, with the dynamic aspects associated with ongoing streams of request...
Aldric Degorre, Oded Maler
FORMATS
2008
Springer
14 years 8 days ago
Timed Parity Games: Complexity and Robustness
We consider two-player games played in real time on game structures with clocks and parity objectives. The games are concurrent in that at each turn, both players independently pro...
Krishnendu Chatterjee, Thomas A. Henzinger, Vinaya...