enter search term and/or author name
A counterexample-guided abstraction-refinement framework for markov decision processes
Rohit Chadha, Mahesh Viswanathan
Article No.: 1
The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of counterexample guided abstraction refinement (CEGAR),...
Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable states of a system requires acceleration techniques that can...
Monadic datalog over finite structures of bounded treewidth
Georg Gottlob, Reinhard Pichler, Fang Wei
Article No.: 3
Bounded treewidth and monadic second-order (MSO) logic have proved to be key concepts in establishing fixed-parameter tractability results. Indeed, by Courcelle's Theorem we know that any property of finite structures, which is expressible by an...
Optimality of size-degree tradeoffs for polynomial calculus
Nicola Galesi, Massimo Lauria
Article No.: 4
There are methods to turn short refutations in polynomial calculus (Pc) and polynomial calculus with resolution (Pcr) into refutations of low degree. Bonet and Galesi [1999, 2003] asked if such size-degree tradeoffs for Pc [Clegg et...
Unicast and multicast QoS routing with soft-constraint logic programming
Stefano Bistarelli, Ugo Montanari, Francesca Rossi, Francesco Santini
Article No.: 5
We present a formal model to represent and solve the unicast/multicast routing problem in networks with quality-of-service (QoS) requirements. To attain this, first we translate the network adapting it to a weighted graph (unicast) or...
Defeasible reasoning is a computationally simple nonmonotonic reasoning approach that has attracted significant theoretical and practical attention. It comprises a family of logics that capture different intuitions, among them ambiguity...
Efficient generation of craig interpolants in satisfiability modulo theories
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Article No.: 7
The problem of computing Craig interpolants has recently received a lot of interest. In this article, we address the problem of efficient generation of interpolants for some important fragments of first-order logic, which are amenable for...
A theory of sampling for continuous-time metric temporal logic
Carlo A. Furia, Matteo Rossi
Article No.: 8
This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of metric temporal logic (MTL) formulas over continuous-time...