enter search term and/or author name
In existing simulation proof techniques, a single step in a lower-level specification may be simulated by an extended execution fragment in a higher-level one. As a result, it is cumbersome to mechanize these techniques using general-purpose...
Abstract versus concrete computation on metric partial algebras
J. V. Tucker, J. I. Zucker
In the theory of computation on topological algebras there is a considerable gap between so-called abstract and concrete models of computation. In concrete models, unlike abstract models, the computations depend on the representation of the...
NEXP TIME-complete description logics with concrete domains
Concrete domains are an extension of Description Logics (DLs) that allow one to integrate reasoning about conceptual knowledge with reasoning about "concrete qualities" of real-world entities such as their sizes, weights, and durations. In this...
Proving correctness of timed concurrent constraint programs
Frank S. De Boer, Maurizio Gabbrielli, Maria Chiara Meo
A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These...
Interval constraint solving for camera control and motion planning
Frédéric Benhamou, Frédéric Goualard, Éric Languénou, , Marc Christie
Many problems in robust control and motion planning can be reduced to either finding a sound approximation of the solution space determined by a set of nonlinear inequalities, or to the "guaranteed tuning problem" as defined by Jaulin and Walter,...