enter search term and/or author name
A classification of symbolic transition systems
Thomas A. Henzinger, Rupak Majumdar, Jean-François Raskin
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...
Making abstract domains condensing
Roberto Giacobazzi, Francesco Ranzato, Francesca Scozzari
In this article, we show that reversible analyses of logic languages by abstract interpretation can be performed without loss of precision by systematically refining abstract domains. This is obtained by adding to the abstract domain the minimal...
On equivalence and canonical forms in the LF type theory
Robert Harper, Frank Pfenning
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality are based on a confluent, strongly normalizing...
A new decidability technique for ground term rewriting systems with applications
Rakesh Verma, Ara Hayrapetyan
Programming language interpreters, proving equations (e.g. x3 = x implies the ring is Abelian), abstract data types, program transformation and optimization, and even computation itself (e.g., turing machine) can all be...
A modal logic framework for multi-agent belief fusion
This article provides a modal logic framework for reasoning about multi-agent belief and its fusion. We propose logics for reasoning about cautiously merged agent beliefs that have different degrees of reliability. These logics are obtained by...
Eternity variables to prove simulation of specifications
Wim H. Hesselink
Simulations of specifications are introduced as a unification and generalization of refinement mappings, history variables, forward simulations, prophecy variables, and backward simulations. A specification implements another specification if and...