TY - JOUR
AB - We prove that for any set S of n points in the plane and n3-α triangles spanned by the points in S there exists a point (not necessarily in S) contained in at least n3-3α/(c log5 n) of the triangles. This implies that any set of n points in three-dimensional space defines at most {Mathematical expression} halving planes.
AU - Aronov, Boris
AU - Chazelle, Bernard
AU - Herbert Edelsbrunner
AU - Guibas, Leonidas J
AU - Sharir, Micha
AU - Wenger, Rephael
ID - 4062
IS - 1
JF - Discrete & Computational Geometry
TI - Points and triangles in the plane and halving planes in space
VL - 6
ER -
TY - CONF
AB - We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of concurrent and reactive systems. A global, discrete, and asynchronous clock is incorporated into the model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upperbound real-time requirements for transitions. We show how to model real-time systems that communicate either through shared variables or by message passing, and how to represent the important real-time constructs of priorities (interrupts), scheduling, and timeouts in this framework. Two styles for the specification of real-time properties are presented. The first style uses bounded versions of the temporal operators; the real-time requirements expressed in this style are classified ...
AU - Thomas Henzinger
AU - Manna, Zohar
AU - Pnueli,Amir
ID - 4508
TI - Temporal proof methodologies for real-time systems
ER -
TY - THES
AU - Thomas Henzinger
ID - 4516
TI - The Temporal Specification and Verification of Real-time Systems
ER -
TY - JOUR
AU - Alur, Rajeev
AU - Thomas Henzinger
ID - 4592
IS - 3
JF - SIGACT News
TI - Time for logic
VL - 22
ER -
TY - CONF
AU - Alur, Rajeev
AU - Feder, Tomás
AU - Thomas Henzinger
ID - 4621
TI - The benefits of relaxing punctuality
ER -