enter search term and/or author name
Checking timed Büchi automata emptiness on simulation graphs
Article No.: 15
Timed automata [Alur and Dill 1994] comprise a popular model for describing real-time and embedded systems and reasoning formally about them. Efficient model-checking algorithms have been developed and implemented in tools such as Kronos [Daws et...
LTL with the freeze quantifier and register automata
Stéphane Demri, Ranko Lazić
Article No.: 16
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier,...
Generalizing consistency and other constraint properties to quantified constraints
Lucas Bordeaux, Marco Cadoli, Toni Mancini
Article No.: 17
Quantified constraints and Quantified Boolean Formulae are typically much more difficult to reason with than classical constraints, because quantifier alternation makes the usual notion of solution inappropriate. As a consequence, basic...
Analytic tableaux calculi for KLM logics of nonmonotonic reasoning
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato
Article No.: 18
We present tableau calculi for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative, and rational logics. Our...
We introduce an algebra qCCS of pure quantum processes in which communications by moving quantum states physically are allowed and computations are modeled by super-operators, but no classical data is explicitly involved. An operational semantics...
Simultaneous checking of completeness and ground confluence for algebraic specifications
Article No.: 20
Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a...
Tableau calculus for preference-based conditional logics: PCL and its extensions
Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Camilla Schwind
Article No.: 21
We present a tableau calculus for some fundamental systems of propositional conditional logics. We consider the conditional logics that can be characterized by preferential semantics (i.e., possible world structures equipped with a family...
We present a redevelopment of the theory of real-valued recursive functions that was introduced by C. Moore in 1996 by analogy with the standard formulation of the integer-valued recursive functions. While his work opened a new line of research on...