We present a technique for the automated verification of abstract models of multithreaded programs providing fresh name generation, name mobility, and unbounded control. As high level specification language we adopt here an extension of communication finite-state machines with local variables ranging over an infinite name domain, called TDL programs. Communication machines have been proved very effective for representing communication protocols as well as for representing abstractions of multithreaded software. The verification method that we propose is based on the encoding of TDL programs into a low level language based on multiset rewriting and constraints that can be viewed as an extension of Petri Nets. By means of this encoding, the symbolic verification procedure developed for the low level language in our previous work can now be applied to TDL programs. Furthermore, the encoding allows us to isolate a decidable class of verification problems for TDL programs that still provide fresh name generation, name mobility, and unbounded control. Our syntactic restrictions are in fact defined on the internal structure of threads: In order to obtain a complete and terminating method, threads are only allowed to have at most one local variable (ranging over an infinite domain of names).

Combining a set of existing constraint solvers into an integ rated system of cooperating solvers is a useful and economic principle to solve hybrid constraint problems. In this paper we show that this approach can also be used to integrate differ ent language paradigms into a unified framework. Furthermore, we study the syntacti c, semantic and operational impacts of this idea for the amalgamation of declarative and constraint programming. To appear in Theory and Practice of Logic Programming (TPLP).

Constraint Programming (CP)[1] has been successfully appl ied to both constraint satisfaction and constraint optimization prob lems. A wide variety of specialized global constraints provide critical assistan ce in achieving a good model that can take advantage of the structure of the problem in the search for a solution. However, a key outstanding issue is the representation of'a d-hoc' constraints that do not have an inherent combinatorial nature, and hence are n ot modelled well using narrowly specialized global constraints. We attempt to address this issue by considering a hybrid of search and compilation. Specificall y we suggest the use of Reduced Ordered Multi-V alued Decision Diagrams (ROMDDs) as the supporting data structure for a generic global constraint. We g ive an algorithm for maintaining generalized arc consistency (GAC) on this cons traint that amortizes the cost of the GAC computation over a root-to-leaf path in th e search tree without requiring asymptotically more space than used for the MD D. Furthermore we present an approach for incrementally maintaining the redu ced property of the MDD during the search, and show how this can be used for provid ing domain entailment detection. Finally we discuss how to apply our ap proach to other similar data structures such as AOMDDs and Case DAGs. The techni que used can be seen as an extension of the GAC algorithm for the regular la nguage constraint on finite length input [2].

Arithmetic constraints on integer intervals are supported in many constraint programming systems. We study here a number of approaches to implement constraint propagation for these constraints. To describe them we introduce integer interval arithmetic. Each approach is explained using appropriate proof rules that reduce the variable domains. We compare these approaches using a set of benchmarks. For the most promising approach we provide results that characterize the effect of constraint propagation. This is a full version of our earlier paper, cs.PL/0403016.

We study the connection between the order of phase transitions in combinatorial problems and the complexity of decision algorithms for such problems. We rigorously show that, for a class of random constraint satisfaction problems, a limited connection between the two phenomena indeed exists. Specifically, we extend the definition of the spine order parameter of Bollobas et al. to random constraint satisfaction problems, rigorously showing that for such problems a discontinuity of the spine is associated with a $2^{Ω(n)}$ resolution complexity (and thus a $2^{Ω(n)}$ complexity of DPLL algorithms) on random instances. The two phenomena have a common underlying cause: the emergence of ``large'' (linear size) minimally unsatisfiable subformulas of a random formula at the satisfiability phase transition. We present several further results that add weight to the intuition that random constraint satisfaction problems with a sharp threshold and a continuous spine are ``qualitatively similar to random 2-SAT''. Finally, we argue that it is the spine rather than the backbone parameter whose continuity has implications for the decision complexity of combinatorial problems, and we provide experimental evidence that the two parameters can behave in a different manner.

This paper advocates the use of a portfolio of representations for problem solving in complex domains. It describes an approach that decouples efficient storage mechanisms called descriptives from the decision-making procedures that employ them. An architecture that takes this approach can learn which representations are appropriate for a given problem class. Examples of search with a portfolio of representations are drawn from a broad set of domains.

LODE is a web tool for children that are novice readers, and is primarily meant for deaf children. It proposes written stories and interactive games for reasoning, globally, on the stories. In this paper, first, we motivate the rationale of LODE, and explain its reasoning games. Then we briefly describe the design of the web client-server architecture of LODE; the server employs a constraint programming system for creating and solving the LODE games in real time. Finally, we concentrate on two evaluations of the latest prototype of LODE: one with hearing novice readers; another one with deaf readers. We conclude by discussing the results of the evaluations, and their implications for LODE.

When configuring customizable software, it is useful to provide interactive tool-support that ensures that the configuration does not breach given constraints. But, when is a configuration complete and how can the tool help the user to complete it? We formalize this problem and relate it to concepts from non-monotonic reasoning well researched in Artificial Intelligence. The results are interesting for both practitioners and theoreticians. Practitioners will find a technique facilitating an interactive configuration process and experiments supporting feasibility of the approach. Theoreticians will find links between well-known formal concepts and a concrete practical application.

LSCS is a satellite workshop of the international conference on principles and practice of Constraint Programming (CP), since 2004. It is devoted to local search techniques in constraint satisfaction, and focuses on all aspects of local search techniques, including: design and implementation of new algorithms, hybrid stochastic-systematic search, reactive search optimization, adaptive search, modeling for local-search, global constraints, flexibility and robustness, learning methods, and specific applications.

Using constraint-based local search, we effectively model and efficiently solve the problem of balancing the traffic demands on portions of the European airspace while ensuring that their capacity constraints are satisfied. The traffic demand of a portion of airspace is the hourly number of flights planned to enter it, and its capacity is the upper bound on this number under which air-traffic controllers can work. Currently, the only form of demand-capacity balancing we allow is ground holding, that is the changing of the take-off times of not yet airborne flights. Experiments with projected European flight plans of the year 2030 show that already this first form of demand-capacity balancing is feasible without incurring too much total delay and that it can lead to a significantly better demand-capacity balance.