Alessandra Di Pierro

Main works - abstracts

Journals

Tempus Fugit: How to Plug It (With C. Hankin and H. Wiklicky) Journal of Logic and Algebraic Programming PDF available.: ABSTRACT
Secret or private information may be leaked to an external attacker through the timing behaviour of the system running the untrusted code. After introducing a formalisation of this situation in terms of a confinement property, we present an algorithm which is able to transform the system into one that is computationally equivalent to the given system but free of timing leaks.
Reversible Combinatory Logic (With C. Hankin and H. Wiklicky) Mathematica Struct. in Computer Science PDF available.: ABSTRACT
The λ-calculus is destructive: its main computational mechanism -- beta reduction -- destroys the redex and makes it thus impossible to replay the computational steps. Combinatory logic is a variant of the λ-calculus which maintains irreversibility. Recently, reversible computational models have been studied mainly in the context of quantum computation, as (without measurements) quantum physics is inherently reversible. However, reversibility also changes fundamentally the semantical framework in which classical computation has to be investigated. We describe an implementation of classical combinatory logic into a reversible calculus for which we present an algebraic model based on a generalisation of the notion of group
Quantitative Static Analysis of Distributed Systems (With C. Hankin and H. Wiklicky) Journal of Functional Programming PDF available.: ABSTRACT
We introduce a quantitative approach to the analysis of distributed systems which relies on a linear operator based network semantics. A typical problem in a distributed setting is how information propagates through a network, and a typical qualitative analysis is concerned with establishing whether some information will eventually be transmitted from one node to another node in the network. The quantitative approach we present allows to obtain additional information such as an estimation of the probability that some data is transmitted within a given interval of time. We formalise situations like this using a probabilistic version of a process calculus which is the core of KLAIM, a language for distributed and mobile computing based on interactions through distributed tuple spaces. The analysis we present exploits techniques based on Probabilistic Abstract Interpretation and is characterised by compositional aspects which greatly simplify the inspection of the nodes interaction and the detection of the information propagation through a computer network.
Probabilistic Lambda-calculus and Quantitative Program Analysis (With C. Hankin and H. Wiklicky) Journal of Logic and Computation PDF available.: ABSTRACT
We show how the framework of probabilistic abstract interpretation can be applied to statically analyse a probabilistic version of the λ-calculus. The resulting analysis allows for a more speculative use of its outcomes based on the consideration of statistically defined quantities. After introducing a linear operator based semantics for our probabilistic λ-calculus &Lambda_P, and reviewing the framework of abstract interpretation and strictness analysis, we demonstrate our technique by constructing a probabilistic (first-order) strictness analysis for &Lambda_P.
Measuring the Confinement of Probabilistic Systems (With C. Hankin and H. Wiklicky) Theoretical Computer Science PDF available.: ABSTRACT
In this paper we lay the semantic basis for a quantitative security analysis of probabilistic systems by introducing notions of approximate confinement based on various process equivalences. We re-cast the operational semantics classically expressed via probabilistic transition systems (PTS) in terms of linear operators and we present a technique for defining approximate semantics as probabilistic abstract interpretations of the PTS semantics. An operator norm is then used to quantify this approximation. This provides a quantitative measure &epsilon of the indistinguishability of two processes and therefore of their confinement. In this security setting a statistical interpretation is then given of the quantity &epsilon which relates it to the number of tests needed to breach the security of the system.
Approximate Non-Interference (With C. Hankin and H. Wiklicky) Journal of Computer Security, 12(1):37-81, 2004. Postscript available.: ABSTRACT
We address the problem of characterising the security of a program against unauthorised information flows. Classical approaches are based on non-inter\-ference models which depend ultimately on the notion of process equivalence. In these models confidentiality is an absolute property stating the absence of any illegal information flow. We present a model in which the notion of non-interference is approximated in the sense that it allows for some exactly quantified leakage of information. This is characterised via a notion of process similarity which replaces the indistinguishability of processes by a quantitative measure of their behavioural difference. Such a quantity is related to the number of statistical tests needed to distinguish two behaviours. We also present two semantics-based analyses of approximate non-interference and we show that one is a correct abstraction of the other.

A preliminary version of this paper appeared in the proceedings of CSFW 2002 and WITS 2002.
Nondeterminism and Infinite Computations in Constraint Programming. (With F.S. de Boer and C. Palamidessi) Theoretical Computer Science, 151:37-78, 1995. Postscript available.: ABSTRACT
We investigate the semantics of concurrent constraint programming and of various sublanguages, with particular emphasis on nondeterminism and infinite behavior. The aim is to find out what is the minimal structure which a domain must have in order to capture these two aspects. We show that a notion of observables, obtained by the upward-closure of the results of computations, is relatively easy to model even in presence of synchronization. On the contrary modeling the exact set of results is problematic, even for the simple sublanguage of constraint logic programming. We show that most of the standard topological techniques fail in capturing this more precise notion of observables. The analysis of these failed attempts leads us to consider a categorical approach.
An algebraic perspective of constraint logic programming. (With F.S. de Boer and C. Palamidessi) Journal of Logic and Computation, 7(1), 1997. Postscript available.: ABSTRACT
We develop a denotational, fully abstract semantics for constraint logic programming (clp) with respect to successful and failed observables. The denotational approach turns out very useful for the definition of new operators on the language as the counterpart of some abstract operations on the denotational domain. In particular, by defining our domain as a cylindric Heyting algebra, we can exploit, to this aim, operations of both cylindric algebras (such as cylindrification), and Heyting algebras (such as implication and negation). The former allows us to generalize the clp language by introducing an explicit hiding operator; the latter allows us to define a notion of negation which extends the classical negation used in Logic Programming. In particular, we show that our notion subsumes both Negation as Failure and Negation as Instantiation.

A preliminary version of this paper, with title A Logical Denotational Semantics for Constraint Logic Programming, appeared in the proceedings of ESOP 94.
Negation as Instantiation. (With M. Martelli and C. Palamidessi.) Information and Computation, 120(2):263-278, 1995. Postscript available.: ABSTRACT
We propose a new negation rule for logic programming which derives existentially closed negative literals, and we define a version of completion for which this rule is sound and complete. The rule is called "Negation As Instantiation" (NAI). According to it, a negated atom succeeds whenever all the branches of the SLD-tree for the atom either fail or instantiate the atom. The set of the atoms whose negation is inferred by the NAI rule is proved equivalent to the complement of $T_c\!\downarrow\!\omega$, where $T_c$ is the immediate consequence operator extended to non-ground atoms (Falaschi et al., 1989). The NAI rule subsumes negation as failure on ground atoms, it excludes floundering and can be efficiently implemented. We formalize this way of handling negation in terms of SLDNI-resolution (SLD-resolution with Negation as Instantiation). Finally, we amalgamate SLDNI-resolution and SLDNF-resolution, thus obtaining a new resolution procedure which is able to treat negative literals with both existentially quantified variables and free variables, and we prove its correctness.

A preliminary version of this paper, with title Negation As Instantiation: a New Rule for the Treatment of Negation in Logic Programming, appeared in the proceedings of ICLP 91.
See also An algebraic perspective of constraint logic programming.

International Conferences

Semantic Abstraction and Quantum Computation (With H. Wiklicky) Pdf available.: ABSTRACT
We present a logico-algebraic approach to probabilistic abstract interpretation based on the ortholattice structure of the projective measurement operators in quantum mechanics. On this base, we present a novel interpretation of quantum measurement as a probabilistic abstraction showing that the measurement of a physical observable essentially corresponds to a static analysis of the observed property.
Abstract Interpretation for Worst and Average Case Analysis (With C. Hankin and H. Wiklicky) Pdf available.: ABSTRACT
We review Wilhelm's work on WCET for hard real-time applications and also recent work on analysis of soft-real time systems using probabilistic methods. We then present Probabilistic Abstract Interpretation (PAI) as a quantitative variation of the classical approach; PAI aims to provide close approximations -- this should be contrasted to the safe approximations studied in the standard setting. We discuss the relation between PAI and classical Abstract Interpretation as well as average case analysis.
Probabilistic Chemical Abstract Machine and the Expressiveness of Linda Languages (With C. Hankin and H. Wiklicky) Pdf available.: ABSTRACT
The Chemical Abstract Machine of Berry and Boudol provides a commonly accepted, uniform framework for describing the operational semantics of various process calculi and languages, such as for example CCS, the pi-calculus and coordination languages like Linda. In its original form the CHAM is purely non-deterministic and thus only describes what reactions are {\em possible} but not how long it will take (in the average) before a certain reaction takes place or its probability. Such quantitative information is however often vital for ``real world'' applications such as systems biology or performance analysis. We propose a probabilistic version of the CHAM. We then define a linear operator semantics for the probabilistic CHAM which exploits a tensor product representation for distributions over possible solutions. Based on this we propose a novel approach towards comparing the expressive power of different calculi via their encoding in the probabilistic CHAM. We illustrate our approach by comparing the expressiveness of various Linda Languages.
Noninterference and the Most Powerful Probabilistic Adversary (With A. Aldini) Pdf available.: ABSTRACT
Probabilistic noninterference extends the classical possibilistic notion introduced by Goguen and Meseguer in order to capture the information leakage caused by adversaries that set up probabilistic covert channels. In this setting we investigate how to evaluate the observational power of an adversary to the purpose of establishing the maximal security degree of a given system. We introduce three classes of probabilistic adversaries, which represent the different observational power of an adversary, and then we establish properties for each such classes which state the complexity of effectively computing the most powerful adversary.
On Reversible Combinatory Logic (With C. Hankin and H. Wiklicky) Pdf available.: ABSTRACT
The lambda calculus is destructive: its main computational mechanism -- beta reduction -- destroys the redex and makes it thus impossible to replay the computational steps. Recently, reversible computational models have been studied mainly in the context of quantum computation, as (without measurements) quantum physics is inherently reversible. However, reversibility also changes fundamentally the semantical framework in which classical computation has to be investigated. We describe an implementation of classical combinatory logic into a reversible calculus for which we present an algebraic model based on a generalisation of the notion of group.
Probabilistic Linda-based Coordination Languages. (With C. Hankin and H. Wiklicky) Pdf available.: ABSTRACT
Coordination languages are intended to simplify the development of complex software systems by separating the coordination aspects of an application from its computational aspects. Coordination refers to the ways the independent active pieces of a program (e.g. a process, a task, a thread, etc.) communicate and synchronise with each other. We review various approaches to introducing probabilistic or stochastic features in coordination languages. The main objective of such a study is to develop a semantic basis for a quantitative analysis of systems of interconnected or interacting components, which allows us to address not only the functional (qualitative) aspects of a system behaviour but also its non-functional aspects, typically considered in the realm of performance modelling and evaluation.
Operator Algebras and the Operational Semantics of Probabilistic Languages. (With H. Wiklicky) Pdf available.: ABSTRACT
We investigate the construction of linear operators representing the semantics of probabilistic programming languages expressed via probabilistic transition systems. Finite transition relations, corresponding to finite automata, can easily be represented by finite dimensional matrices; for the infinite case we need to consider an appropriate generalisation of matrix algebras. We argue that C star algebras, or more precisely Approximately Finite (or AF) algebras, provide a sufficiently rich mathematical structure for modelling probabilistic processes. We show how to construct for a given probabilistic language a unique AF~algebra A and how to represent the operational semantics of processes within this framework: finite computations correspond directly to operators in A, while infinite processes are represented by elements in the so-called strong closure of this algebra.
Continuous-Time Probabilistic KLAIM. (With C. Hankin and H. Wiklicky) Pdf available.: ABSTRACT
We present a probabilistic version of KLAIM, which we call pKLAIM. At the local level, we introduce probabilistic parallel and choice operators. In addition we use probabilistic allocation environments which associate distributions on physical sites with logical localities. Furthermore, we associates a rate with each node; this determines how often a node is active. An alternative would be to associate a probability with each node, indicating the chance that a process at that node will be selected for execution. We have studied such a variant in detail in an earlier paper.
On Quantitative Analysis of Probabilistic Protocols. (With A. Aldini) Pdf available.: ABSTRACT
We advocate the use of approximate noninterference for the security analysis of probabilistic protocols. Our approach relies on a formalisation of the protocol in the setting of a probabilistic process algebra and a notion of process similarity based on weak probabilistic bisimulation. We illustrate this approach by presenting the analysis of a probabilistic nonrepudiation protocol which allows us to quantitatively estimate its fairness degree.
Probabilistic KLAIM. (With C. Hankin and H. Wiklicky) Postscript available.: ABSTRACT
We introduce a probabilistic extension of KLAIM, where the behaviour of networks and individual nodes is determined by a probabilistic scheduler for processes and probabilistic allocation environments which describe the logical neighbourhood of each node. The resulting language has two variants which are modelled respectively as discrete and continuous time Markov processes. We suggest that Poisson processes are a natural probabilistic model for the coordination of discrete processes asynchronously communicating in continuous time and we use them to define the operational semantics of the continuous time variant. This framework allows for the implementation of networks with independent clocks on each site.
A Quantitative Approach to Noninterference for Probabilistic Systems. (With A. Aldini) Postscript available.: ABSTRACT
We present a technique for measuring the security of a system which relies on a probabilistic process algebraic formalisation of noninterference. We define a mathematical model for this technique which consists of a linear space of processes and linear transformations on them. In this model the measured quantity corresponds to the norm of a suitably defined linear operator associated to the system. The probabilistic model we adopt is reactive in the sense that processes can react to the environment with a probabilistic choice on a set of inputs; it is also generative in the sense that outputs autonomously chosen by the system are governed by a probability distribution. In this setting, noninterference is formulated in terms of a probabilistic notion of weak bisimulation. We show how the probabilistic information in this notion can be used to estimate the maximal information leakage, i.e. the security degree of a system against a most powerful attacker.
Quantitative Relations and Approximate Process Equivalences. (With C. Hankin and H. Wiklicky) Postscript available.: ABSTRACT
We introduce a characterisation of probabilistic transition systems (PTS) in terms of linear operators on some suitably defined vector space representing the set of states. Various notions of process equivalences can then be re-formulated as abstract linear operators related to the concrete PTS semantics via a probabilistic abstract interpretation. These process equivalences can be turned into corresponding approximate notions by identifying processes whose abstract operators ``differ'' by a given quantity, which can be calculated as the norm of the difference operator. We argue that this number can be given a statistical interpretation in terms of the tests needed to distinguish two behaviours.
Measuring the Confinement of Concurrent Probabilistic Systems. (With C. Hankin and H. Wiklicky) Postscript available.: ABSTRACT
In previous work we have studied the notion of approximate confinement based on I/O observables. In this paper, we generalise this work to consider probabilistic bisimulation (both exact and approximate) in the context of probabilistic transition systems. We also show the relationship between probabilistic bisimulation and probabilistic abstract interpretation; this result parallels Schmidt's result in the classical (non-probabilistic) setting where he relates bisimulation and Galois connections. We conclude with some examples.
Linear Embedding for a Quantitative Comparison of Language Expressiveness. (With A. Brogi and H. Wiklicky) Postscript available.: ABSTRACT
We introduce the notion of linear embedding which refines Shapiro's notion of embedding by recasting it in a linear-space based semantics setting. We use this notion to compare the expressiveness of a class of languages that employ asynchronous communication primitives à la Linda. The adoption of a linear semantics in which the observables of a language are linear operators (matrices) representing the programs transition graphs allows us to give quantitative estimates of the different expressive power of languages, thus improving previous results in the field.
Probabilistic Abstract Interpretation and Statistical Testing. (With H. Wiklicky) Postscript available.: ABSTRACT
Although generally too weak to guarantee correctness, testing is an indispensable technique for the validation of reactive systems. Abstract Interpretation has been used to overcome some of the problems associated with testing such as the termination of a program run within an acceptable interval of time. We propose the use of Probabilistic Abstract Interpretation for measuring the error made in the evaluation of the reliability of systems via Monte-Carlo testing. The problem we consider is to determine the probability that a reactive system's response falls within a certain set of possible outputs, i.e. that it passes a certain test. As Monte-Carlo testing of the concrete system is not always feasible, tests can be performed instead on an abstract system. This abstraction introduces a further approximation which must be taken into account in the estimation of the error made by testing. The problem is to find out how much the expectation value (or average) of the abstract system differs from the one of the concrete system. We show how to measure such difference by lifting the abstraction to a probabilistic abstract interpretation.
Analysing Approximate Confinement under Uniform Attacks. (With C. Hankin and H. Wiklicky) Postscript available.: ABSTRACT
We are concerned to give certain guarantees about the security of a system. We identify two kinds of attack: the internally scheduled attack (exemplified by Trojan Horse attacks) and externally scheduled attacks (exemplified by timing attacks). In this paper we focus on the latter. We present a semantic framework for studying such attacks in the context of PCCP, a simple process algebra with a constraint store. We show that a measure of the efficacy of an attacker can be determined by considering its observable behaviour over the "average" store of the system (for some number of steps). We show how to construct an analysis to determine the average store using the technique of probabilistic abstract interpretation.
Approximate Non-Interference. (With C. Hankin and H. Wiklicky) Postscript available.: ABSTRACT
We address the problem of characterising the security of a program against unauthorised information flows. Classical approaches are based on non-interference models which depend ultimately on the notion of process equivalence. In these models confidentiality is an absolute property stating the absence of any illegal information flow. We present a model in which the notion of non-interference is approximated in the sense that it allows for some exactly quantified leakage of information. This is characterised via a notion of process similarity which replaces the indistinguishability of processes by a quantitative measure of their behavioural difference. Such a quantity is related to the number of statistical tests needed to distinguish two behaviours. We also present two semantics-based analyses of approximate non-interference and we show that one is a correct abstraction of the other.
Quantum Constraint Programming . (With H. Wiklicky) Postscript available.: ABSTRACT
Quantum computers are hypothetical machines which can perform many calculations simultaneously based on quantum-mechanical principles that allows a single bit to coexist in many states at once. This enormous potential of quantum computing has attracted substantial interest, especially during the last decade, and initiated a whole new field of research. As a contribution to this research we address the problem of the design of high level languages for programming quantum computers, and the definition of an appropriate formal semantics for such languages. To this purpose we consider the Constraint Programming paradigm and we show how computations in this paradigm can be seen as physical processes obeying the laws of quantum mechanics.
Linear Stuctures for Concurrency in Probabilistic Programming Languages . (With H. Wiklicky) Postscript available.: ABSTRACT
We introduce a semantical model based on operator algebras and we show the suitability of this model to capture both a quantitative version of non-determinism (in the form of a probabilistic choice) and concurrency. We present the model by referring to a generic language which generalises various probabilistic concurrent languages from different programming paradigms. We discuss the relation between concurrency and the commutativity of the resulting semantical domain. In particular, we use Gelfand's representation theorem to relate the semantical models of synchronisation-free and fully concurrent versions of the language. A central aspect of the model we present is that it allows for a unified view of both operational and denotational semantics for a concurrent language.
Probabilistic Confinement in a Declarative Framework. (With H. Wiklicky and Chris Hankin) Postscript available.: ABSTRACT
We show how to formulate and investigate security notions in the context of declarative programming. We concentrate on a particular class of security properties, namely the one called in \cite{VolpanoSmith98a} {\em confinement} properties. Our reference language is concurrent constraint programming. We use a probabilistic version of this language to highlight via simple programs examples the difference between probabilistic and non-deterministic confinement as pointed out in the work by Volpano and Smith \cite{VolpanoSmith98b,VolpanoSmith98c} in the context of imperative languages. The different role played by variables in imperative and constraint programming hinders a direct translation of the notion of confinement into our declarative setting. Therefore, we introduce the notion of ``identity confinement'' which is more appropriate for constraint languages. Finally, we present an approximating probabilistic semantics which can be used as a base for the analysis of confinement properties.
Measuring the Precision of Abstract Interpretations. (With H. Wiklicky.) Postscript available.: ABSTRACT
We present a method for approximating the semantics of probabilistic programs to the purpose of constructing semantics-based analyses of various properties. The method is also suited for a probabilistic analysis of classical deterministic programs. The framework resembles the one based on Galois connection used in abstract interpretation, the main difference being the choice of linear space structures instead of order-theoretic ones as semantical (concrete and abstract) domains. Linear spaces reflect the quantitative aspects of (probabilistic) computation and are therefore of fundamental importance in the semantics and the semantics-based analysis. The intrinsic quantitative nature of linear spaces makes the method suitable for investigations on the problem of a numerical comparison of abstract interpretations with respect to their precision.
Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation. (With H. Wiklicky.) Postscript available.: ABSTRACT
We present a method for approximating the semantics of probabilistic programs to the purpose of constructing semantics-based analyses of such programs. The method resembles the one based on Galois connection as developed in the Cousot framework for abstract interpretation. The main difference between our approach and the standard theory of abstract interpretation is the choice of linear space structures instead of order-theoretic ones as semantical (concrete and abstract) domains. We show that our method generates ``best approximations'' according to an appropriate notion of precision defined in terms of a norm. Moreover, if re-casted in a order-theoretic setting these approximations are correct in the sense of classical abstract interpretation theory. We use Concurrent Constraint Programming as a reference programming paradigm. The basic concepts and ideas can nevertheless be applied to any other paradigm. The results we present are intended to be the first step towards a general theory of probabilistic abstract interpretation, which re-formulates the classical theory in a setting suitable for a quantitative reasoning about programs.
Randomised Algorithms and Probabilistic Constraint Programming. (With H. Wiklicky.) Postscript available.: ABSTRACT
We propose a declarative implementation of randomised algorithms, which exploits the Constraint Logic Programming (CLP) paradigm. For the high-level formalisation of probabilistic programs expressing such algorithms we actually refer to a generalisation of CLP, namely the Probabilistic Concurrent Constraint Programming (PCCP) language, previously introduced by the authors. This language provides a construct for probabilistic choice which allows us to express randomness in a program. The design of PCCP does not require any additional structure on the underlying constraint system (e.g. fuzzy or belief systems) and therefore also allows a straight forward implementation. We demonstrate the use of this language for implementing randomised algorithms. In particular, we give an extensive treatment of two popular (generic) randomised algorithms, namely Simulated Annealing and Randomised Rounding, and we discuss some instantiations of these algorithms for solving two well-known optimisation problems, namely the travelling salesman (TSP) and the maximum satisfaction (MAX SAT) problem.
Quantitative Observables and Averages in Probabilistic Constraint Programming. (With H. Wiklicky.) Postscript available.: ABSTRACT
We investigate notions of observable behaviour of programs which include quantitative aspects of computation along with the most commonly assumed qualitative ones. We model these notions by means of a transition system where transitions occur with a given probability and an associated `cost' expressing some complexity measure (e.g. running time or, in general, resource consumption). The addition of these quantities allows for a natural formulation of the {\em average} behaviour of a program, whose specification and analysis is particularly important in the study of system performance and reliability. We base our model on the Concurrent Constraint Programming (CCP) paradigm and we argue that it can be an appropriate base for further developments oriented to the analysis and verification of average properties.
Ergodic Average in Constraint Programming. (With H. Wiklicky.) Postscript available.: ABSTRACT
We will discuss the problem of modelling probabilistic properties of constraint programs, which express the average of some quantities of interest. A random variable on the set of constraints is used for assigning to each constraint a real value representing the `cost' of that constraint. This way, we obtain a notion of quantitative observables Q which, although interesting in itself can be used in order to define different types of average properties.
A Markov Model for Probabilistic Concurrent Constraint Programming. (With H. Wiklicky.) Postscript available.: ABSTRACT
This paper introduces a new approach towards the semantics of Concurrent Constraint Programming (CCP), which is based on operator algebras. In particular, we show how stochastic matrices can be used for modelling both a quantitative version of nondeterminism (in the form of a probabilistic choice) and synchronisation. We will assume Probabilistic Concurrent Constraint Programming (PCCP) as the reference paradigm. The presented model subsumes CCP as a special case. The model is obtained by a fixpoint construction on a space of linear operators. For the purpose of this paper, we consider only finite constraint systems. This allows us to define our model by using finite dimensional linear operators, i.e. matrices. We show that our model is equivalent to a notion of observables which extends the standard one in CCP (input/output behaviour) by including information about the likelihood of the computed results. The model also captures infinite computations. The adoption of functional analytical and operator algebraic methods constitutes the main novelty of this work. It also creates a natural link between (a certain field of) computer science and different disciplines such as physics, by the use of the theory of stochastic processes.
Implementing Randomised Algorithms in Constraint Logic Programming. (With N. Angelopoulos and H. Wiklicky.) Postscript available.: ABSTRACT
We propose a declarative-based implementation of randomised algorithms, which exploits the Constraint Logic Programming (CLP) paradigm. For the high-level formalisation of probabilistic programs expressing such algorithms we actually refer to a generalisation of CLP, namely the Probabilistic Concurrent Constraint Programming (PCCP) language, previously introduced in ICCL98. This language provides a construct for probabilistic choice which allows us to express randomness in a program. PCCP also includes synchronisation and concurrency aspects. However, for the purpose of this work, the (probabilistic) CLP fragment of PCCP is sufficient. We present a meta-interpreter for this language. This is just a standard prolog meta-interpreter, suitably extended so as to deal with probabilistic choice. For the constraint solving, the meta-interpreter exploits existing constraint handling facilities (and in more concrete terms to the SICStus 3.\#6 system). This is possible because the design of PCCP does not require any additional structure on the underlying constraint system (e.g. fuzzy or belief systems). We demonstrate the use of this system for implementing randomised algorithms. In particular, we give an extensive treatment of two popular (generic) randomised algorithms, namely Simulated Annealing and Randomised Rounding, and we discuss some instantiations of these algorithms for solving two well-known optimisation problems, namely the travelling salesman (TSP) and the maximum satisfaction (MAX SAT) problem.
Probabilistic Concurrent Constraint Programming: Towards a Fully Abstract Model. (With H. Wiklicky.) Postscript available.: ABSTRACT
This paper presents a Banach space based approach towards a denotational semantics of a probabilistic constraint programming language. This language is based on the concurrent constraint programming paradigm, where randomness is introduced by means of a probabilistic choice construct. As a result, we obtain a declarative framework, in which randomised algorithms can be expressed and formalised. The denotational model we present is constructed by using functional-analytical techniques. As an example, the existence of fixed-points is guaranteed by the Brouwer-Schauder Fixed-Point Theorem. A concrete fixed-point construction is also presented which corresponds to a notion of observables capturing the exact results of both finite and infinite computations.
An Operational Semantics for Probabilistic Concurrent Constraint Programming . (With H. Wiklicky.) Postscript available.: ABSTRACT
This paper investigates a probabilistic version of the concurrent constraint programming paradigm (CCP). The aim is to introduce the possibility to formulate so called ``randomised algorithms'' within the CCP framework. Differently from common approaches in (imperative) high-level programming languages, which rely on some kind of random() function, we introduce randomness in the very definition of the language by means of a probabilistic choice construct. This allows a program to make stochastic moves during its execution. We call the resulting language Probabilistic Concurrent Constraint Programming (PCCP). We present an operational semantics for PCCP by means of a probabilistic transition system such that the execution of a PCCP program may be seen as a stochastic process, i.e. as a random walk on the transition graph. The transition probabilities are given explicitly. This semantics captures a notion of observables which combines results of computations and the probability of those results being computed. This embedding of randomness within the semantics of a well structured programming paradigm, like CCP, also aims at providing a sound framework for formalising and reasoning about randomised algorithms and programs. Additionally, we give some examples of PCCP programs and we show how well-known randomised algorithms can be implemented very naturally in the new language.
A Banach Space Based Semantics for Probabilistic Concurrent Constraint Programming. (With H. Wiklicky.) Postscript available.: ABSTRACT
The aim of this work is to provide a probabilistic foundation for nondeterministic computations in Concurrent Constraint Programming (CCP). Differently from common approaches in (imperative) high-level programming languages, which rely on some kind of random() function, we introduce randomness in the very definition of the language by means of a probabilistic choice construct. This allows a program to make stochastic moves during its execution. We call the resulting language Probabilistic Concurrent Constraint Programming (PCCP). We present an operational and denotational semantics for PCCP both capturing a notion of observables which combines results of computations and the probability of those results being computed. For the denotational semantics, we consider linear (Banach) structures and the mathematics behind them, as appropriate candidates for the definition of the domain of denotations. This approach differs from the ones typically adopted in the semantics of constraint programming, which are based on order-theoretic or metric structures. We compare this semantics to other approaches and discuss it in some examples.
On Probabilistic CCP . (With H. Wiklicky.) Postscript available.: ABSTRACT
This paper investigates a probabilistic version of the concurrent constraint programming paradigm (CCP). The aim is to introduce the possibility to formulate so called ``randomised algorithms'' within the CCP framework. Our approach incorporates randomness directly within the (operational) semantics instead of referring to an ``external'' function or procedure call. We define the operational semantics of probabilistic concurrent constraint programming (PCCP) by means of a probabilistic transition system such that the execution of a PCCP program may be seen as a stochastic process, i.e. as a random walk on the transition graph. The transition probabilities are given explicitly.
On Negation As Instantiation . (With W. Drabent.) Postscript available.: ABSTRACT
Given a logic program P and a goal G, we introduce a notion which states when an SLD-tree for P and G instantiates a set of variables V with respect to another one, W. We call this notion weak instantiation, as it is a generalization of the instantiation property introduced in a previous work ("Negation As Instantiation"). A negation rule based on instantiation, the so-called Negation As Instantiation rule (NAI), allows for inferring existentially closed negative queries, that is formulas of the form $\exists\neg Q$, from logic programs.
We show that, by using the new notion, we can infer a larger class of negative queries, namely the class of the queries of the form $\forall_W\exists_V\neg Q$ and of the form $\forall_W\exists_V\forall_Z\neg Q$, where $Z$ is the set of the remaining variables of Q.
On Quantified Negative Queries . (With W. Drabent.) Postscript available.: ABSTRACT
Given a logic program P and a goal G, we introduce a notion which states when an SLD-tree for P and G instantiates a set of variables V with respect to another one, W. We call this notion weak instantiation, as it is a generalization of the instantiation property introduced in a previous work ("Negation As Instantiation"). A negation rule based on instantiation, the so-called Negation As Instantiation rule (NAI), allows for inferring existentially closed negative queries, that is formulas of the form $\exists\neg Q$, from logic programs.
We show that, by using the new notion, we can infer a larger class of negative queries, namely the class of the queries of the form $\forall_W\exists_V\neg Q$ and of the form $\forall_W\exists_V\forall_Z\neg Q$, where $Z$ is the set of the remaining variables of Q.

National Conferences

Amalgamating NAF and NAI . Postscript available.: ABSTRACT
We define a new logic language with negation by introducing existential and universal quantifiers in the queries.
Negation is handled by using two rules: the NAF rule for universally quantified negative queries and the NAI rule for existentially quantified negative queries. We formalize this amalgamation in terms of NAIF-resolution (SLD-resolution with Negation As Instantiation and Failure), and we prove its correctness w.r.t. the completion semantics.
We also show how extended programs and goals, i.e. programs and goals whose body is an arbitrary first-order formula, can be transformed into programs and goals in the new language and then evaluated using our system.

PhD Thesis

Negation and Infinite Computations in Logic Programming. Postscript available.: ABSTRACT
This thesis is devoted to probe into some aspects of Logic Programming, namely the problem of inferring some negative information from a logic program, the denotational characterization of the meaning of a program, and the study of its infinite computations. Concerning the first problem, the attention is focused on the negative information expressed by the existential quantification of the negation of an atom (or a conjunction of atoms) which is not a logical consequence of the theory associated to a given logic program. Operationally, these formulas can be inferred by means of the Negation As Instantiation rule; from a logical point of view, they are shown to be exactly those formulas which are logical consequences of the theory obtained by considering the Clark completion of the given program on a universal vocabulary. The paradigm of Logic Programming is then extended by allowing the use of the existential negative expressions in the definition of the predicates, and, correspondingly, also the classical mechanism of SLD-resolution is extended so to deal with the new formulas.
The other two aspects are tackled within the more general framework of constraint logic programming. This language is reformulated in algebraic terms as the free language generated by a BNF grammar. This allows us to define a structured operational semantics, based on a transition system, by means of which a notion of observables is introduced, also including the results of infinite computations. Then, a compositional semantics based on logical operators is defined, and it is shown its full correspondence with the observables. The denotational meaning of the program is obtained by considering the domain of the upward-closed Scott-compact sets of constraints (the Smith powerdomain of the domain of constrains). It turns out that the well-known Negation As Failure of Logic Programming is just the Heyting negation on this domain.