@inproceedings{4367,
author = {Podelski,Andreas and Thomas Wies},
pages = {267 -- 282},
publisher = {Springer},
title = {{Boolean Heaps}},
doi = {1550},
year = {2005},
}
@inproceedings{4404,
author = {Alur, Rajeev and Pavol Cerny and Madhusudan,P. and Nam,Wonhong},
pages = {98 -- 109},
publisher = {ACM},
title = {{Synthesis of interface specifications for Java classes}},
doi = {1542},
year = {2005},
}
@inproceedings{4412,
abstract = {The periodic resource model for hierarchical, compositional scheduling abstracts task groups by resource requirements. We study this model in the presence of dataflow constraints between the tasks within a group (intragroup dependencies), and between tasks in different groups (inter-group dependencies). We consider two natural semantics for dataflow constraints, namely, RTW (real-time workshop) semantics and LET (logical execution time) semantics. We show that while RTW semantics offers better end-to-end latency on the task group level, LET semantics allows tighter resource bounds in the abstraction hierarchy and therefore provides better composability properties. This result holds both for intragroup and intergroup dependencies, as well as for shared and for distributed resources.},
author = {Matic, Slobodan and Thomas Henzinger},
pages = {99 -- 110},
publisher = {IEEE},
title = {{Trading end-to-end latency for composability}},
doi = {10.1109/RTSS.2005.43},
year = {2005},
}
@inproceedings{4418,
abstract = {We present a new software system architecture for the implementation of hard real-time applications. The core of the system is a microkernel whose reactivity (interrupt handling as in synchronous reactive programs) and proactivity (task scheduling as in traditional RTOSs) are fully programmable. The microkernel, which we implemented on a StrongARM processor, consists of two interacting domain-specific virtual machines, a reactive E (Embedded) machine and a proactive S (Scheduling) machine. The microkernel code (or microcode) that runs on the microkernel is partitioned into E and S code. E code manages the interaction of the system with the physical environment: the execution of E code is triggered by environment interrupts, which signal external events such as the arrival of a message or sensor value, and it releases application tasks to the S machine. S code manages the interaction of the system with the processor: the execution of S code is triggered by hardware interrupts, which signal internal events such as the completion of a task or time slice, and it dispatches application tasks to the CPU, possibly preempting a running task. This partition of the system orthogonalizes the two main concerns of real-time implementations: E code refers to environment time and thus defines the reactivity of the system in a hardware- and scheduler-independent fashion; S code refers to CPU time and defines a system scheduler. If both time lines can be reconciled, then the code is called time safe; violations of time safety are handled again in a programmable way, by run-time exceptions. The separation of E from S code permits the independent programming, verification, optimization, composition, dynamic adaptation, and reuse of both reaction and scheduling mechanisms. Our measurements show that the system overhead is very acceptable even for large sets of task, generally in the 0.2--0.3% range.},
author = {Kirsch, Christoph M and Sanvido, Marco A and Thomas Henzinger},
pages = {35 -- 45},
publisher = {ACM},
title = {{A programmable microkernel for real-time systems}},
doi = {10.1145/1064979.1064986},
year = {2005},
}
@article{4454,
abstract = {We define five increasingly comprehensive classes of infinite-state systems, called STS1--STS5, whose state spaces have finitary structure. For four of these classes, we provide examples from hybrid systems.STS1 These are the systems with finite bisimilarity quotients. They can be analyzed symbolically by iteratively applying predecessor and Boolean operations on state sets, starting from a finite number of observable state sets. Any such iteration is guaranteed to terminate in that only a finite number of state sets can be generated. This enables model checking of the μ-calculus.STS2 These are the systems with finite similarity quotients. They can be analyzed symbolically by iterating the predecessor and positive Boolean operations. This enables model checking of the existential and universal fragments of the μ-calculus.STS3 These are the systems with finite trace-equivalence quotients. They can be analyzed symbolically by iterating the predecessor operation and a restricted form of positive Boolean operations (intersection is restricted to intersection with observables). This enables model checking of all ω-regular properties, including linear temporal logic.STS4 These are the systems with finite distance-equivalence quotients (two states are equivalent if for every distance d, the same observables can be reached in d transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new state sets are generated. This enables model checking of the existential conjunction-free and universal disjunction-free fragments of the μ-calculus.STS5 These are the systems with finite bounded-reachability quotients (two states are equivalent if for every distance d, the same observables can be reached in d or fewer transitions). The systems in this class can be analyzed symbolically by iterating the predecessor operation and terminating when no new states are encountered (this is a weaker termination condition than above). This enables model checking of reachability properties.},
author = {Thomas Henzinger and Majumdar, Ritankar S and Raskin, Jean-François},
journal = {ACM Transactions on Computational Logic (TOCL)},
number = {1},
pages = {1 -- 32},
publisher = {ACM},
title = {{A classification of symbolic transition systems}},
doi = {10.1145/1042038.1042039},
volume = {6},
year = {2005},
}
@inproceedings{4455,
abstract = {We define quantitative similarity functions between timed transition systems that measure the degree of closeness of two systems as a real, in contrast to the traditional boolean yes/no approach to timed simulation and language inclusion. Two systems are close if for each timed trace of one system, there exists a corresponding timed trace in the other system with the same sequence of events and closely corresponding event timings. We show that timed CTL is robust with respect to our quantitative version of bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula. We also define a discounted version of CTL over timed systems, which assigns to every CTL formula a real value that is obtained by discounting real time. We prove the robustness of discounted CTL by establishing that close states in the bisimilarity metric have close values for all discounted CTL formulas.},
author = {Thomas Henzinger and Majumdar, Ritankar S and Prabhu, Vinayak S},
pages = {226 -- 241},
publisher = {Springer},
title = {{Quantifying similarities between timed systems}},
doi = {10.1007/11603009_18},
volume = {3829},
year = {2005},
}
@inproceedings{4456,
abstract = {A modular program analysis considers components independently and provides a succinct summary for each component, which is used when checking the rest of the system. Consider a system consisting of a library and a client. A temporal summary, or interface, of the library specifies legal sequences of library calls. The interface is safe if no call sequence violates the library's internal invariants; the interface is permissive if it contains every such sequence. Modular program analysis requires full interfaces, which are both safe and permissive: the client does not cause errors in the library if and only if it makes only sequences of library calls that are allowed by the full interface of the library.Previous interface-based methods have focused on safe interfaces, which may be too restrictive and thus reject good clients. We present an algorithm for automatically synthesizing software interfaces that are both safe and permissive. The algorithm generates interfaces as graphs whose vertices are labeled with predicates over the library's internal state, and whose edges are labeled with library calls. The interface state is refined incrementally until the full interface is constructed. In other words, the algorithm automatically synthesizes a typestate system for the library, against which any client can be checked for compatibility. We present an implementation of the algorithm which is based on the BLAST model checker, and we evaluate some case studies.},
author = {Thomas Henzinger and Jhala, Ranjit and Majumdar, Ritankar S},
pages = {31 -- 40},
publisher = {ACM},
title = {{Permissive interfaces}},
doi = {10.1145/1081706.1081713},
year = {2005},
}
@inproceedings{4457,
abstract = {We present a compositional approach to the implementation of hard real-time software running on a distributed platform. We explain how several code suppliers, coordinated by a system integrator, can independently generate different parts of the distributed software. The task structure, interaction, and timing is specified as a Giotto program. Each supplier is given a part of the Giotto program and a timing interface, from which the supplier generates task and scheduling code. The integrator then checks, individually for each supplier, in pseudo-polynomial time, if the supplied code meets its timing specification. If all checks succeed, then the supplied software parts are guaranteed to work together and implement the original Giotto program. The feasibility of the approach is demonstrated by a prototype implementation.},
author = {Thomas Henzinger and Kirsch, Christoph M and Matic, Slobodan},
pages = {21 -- 30},
publisher = {ACM},
title = {{Composable code generation for distributed Giotto}},
doi = {10.1145/1065910.1065914},
year = {2005},
}
@inproceedings{4536,
abstract = {We show how to automatically construct and refine rectangular abstractions of systems of linear differential equations. From a hybrid automaton whose dynamics are given by a system of linear differential equations, our method computes automatically a sequence of rectangular hybrid automata that are increasingly precise overapproximations of the original hybrid automaton. We prove an optimality criterion for successive refinements. We also show that this method can take into account a safety property to be verified, refining only relevant parts of the state space. The practicability of the method is illustrated on a benchmark case study. },
author = {Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François},
pages = {144 -- 161},
publisher = {Springer},
title = {{Automatic rectangular refinement of affine hybrid systems}},
doi = {DOI: 10.1007/11603009_13},
volume = {3829},
year = {2005},
}
@inproceedings{4541,
abstract = {Much recent research has focused on the applications of games with ω-regular objectives in the control and verification of reactive systems. However, many of the game-based models are ill-suited for these applications, because they assume that each player has complete information about the state of the system (they are “perfect-information” games). This is because in many situations, a controller does not see the private state of the plant. Such scenarios are naturally modeled by “partial-information” games. On the other hand, these games are intractable; for example, partial-information games with simple reachability objectives are 2EXPTIME-complete.
We study the intermediate case of “semiperfect-information” games, where one player has complete knowledge of the state, while the other player has only partial knowledge. This model is appropriate in control situations where a controller must cope with plant behavior that is as adversarial as possible, i.e., the controller has partial information while the plant has perfect information. As is customary, we assume that the controller and plant take turns to make moves. We show that these semiperfect-information turn-based games are equivalent to perfect-information concurrent games, where the two players choose their moves simultaneously and independently. Since the perfect-information concurrent games are well-understood, we obtain several results of how semiperfect-information turn-based games differ from perfect-information turn-based games on one hand, and from partial-information turn-based games on the other hand. In particular, semiperfect-information turn-based games can benefit from randomized strategies while the perfect-information variety cannot, and semiperfect-information turn-based games are in NP ∩ coNP for all parity objectives.
},
author = {Krishnendu Chatterjee and Thomas Henzinger},
pages = {1 -- 18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Semiperfect-information games}},
doi = {10.1007/11590156_1},
volume = {3821},
year = {2005},
}