Search ACM DL

Search Issue

enter search term and/or author name

**A counterexample-guided abstraction-refinement framework for markov decision processes**

Rohit Chadha, Mahesh Viswanathan

Article No.: 1

DOI: 10.1145/1838552.1838553

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)*,...

**On (Omega-)regular model checking**

Axel Legay, Pierre Wolper

Article No.: 2

DOI: 10.1145/1838552.1838554

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

DOI: 10.1145/1838552.1838555

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

DOI: 10.1145/1838552.1838556

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

DOI: 10.1145/1838552.1838557

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...

**An inclusion theorem for defeasible logics**

David Billington, Grigoris Antoniou, Guido Governatori, Michael Maher

Article No.: 6

DOI: 10.1145/1838552.1838558

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

DOI: 10.1145/1838552.1838559

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

DOI: 10.1145/1838552.1838560

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...