Author name cluster

C. Palamidessi

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

TCS Journal 2007 Journal Article

Separation of synchronous and asynchronous communication via testing

D. Cacciagrano
F. Corradini
C. Palamidessi

One of the early results concerning the asynchronous π -calculus which significantly contributed to its popularity is the capability of encoding the output prefix of the (choiceless) π -calculus in a natural and elegant way. Encodings of this kind were proposed by Honda and Tokoro, by Nestmann and (independently) by Boudol. We investigate whether the above encodings preserve De Nicola and Hennessy’s testing semantics. In this sense, it turns out that, under some general conditions, no encoding of the output prefix is able to preserve the must testing. This negative result is due to (a) the non-atomicity of the sequences of steps which are necessary in the asynchronous π -calculus to mimic synchronous communication, and (b) testing semantics’ sensitivity to divergence.

Details DOI

I&C Journal 1995 Journal Article

Negation as Instantiation

A. Dipierro
M. Martelli
C. Palamidessi

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 Tc ↓ ω, where Tc is the immediate consequence operator extended to non-ground atoms (M. Falaschi et al. , 1989, Theoret. Comput, Sci. 69(3), 289-318). 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.

Details DOI

I&C Journal 1994 Journal Article

Embedding as a Tool for Language Comparison

F.S. Deboer
C. Palamidessi

This paper addresses the problem of defining a formal tool to compare the expressive power of different concurrent constraint languages. We refine the notion of embedding by adding some "reasonable" conditions, suitable for concurrent frameworks. The new notion, called modular embedding, is used to define a preorder among these languages, representing different degrees of expressiveness. We show that this preorder is not trivial (i. e. , it does not collapse into one equivalence class) by proving that Flat CP cannot be embedded into Flat GHC, and that Flat GHC cannot be embedded into a language without communication primitives in the guards, while the converses hold.

Details DOI

I&C Journal 1993 Journal Article

A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs

M. Falaschi
G. Levi
M. Martelli
C. Palamidessi

In this paper we define a new notion or truth on Herbrand interpretations extended with variables which allows us to capture, by means of suitable models, various observable properties, such as the ground success set, the set of atomic consequences, and the computed answer substitutions. The notion of truth extends the classical one to account for non-ground formulas in the interpretations. The various operational semantics are all models. An ordering on interpretations is defined to overcome the problem that the intersection of a set of models is not necessarily a model. The set of interpretations with this partial order is shown to be a complete lattice, and the greatest lower bound of any set of models is shown to be a model. Thus there exists a least model, which is the least Herbrand model and therefore the ground success set semantics. Richer operational semantics are non-least models, which can, however, be effectively defined by fixpoint constructions. The model corresponding to the computed answer substitutions operational semantics is the most primitive one (the others can easily be obtained from it).

Details DOI

TCS Journal 1992 Journal Article

From failure to success: comparing a denotational and a declarative semantics for Horn clause logic

F.S. de Boer
J.N. Kok
C. Palamidessi
J.J.M.M. Rutten

The main purpose of the paper is to relate different models for Horn clause logic: operational, denotational, declarative. We study their relationship by contrasting models based on interleaving, on the one hand, to models based on maximal parallelism, on the other. We make use of complete metric spaces as an important mathematical tool, both in defining and in comparing the various models.

Details DOI

TCS Journal 1991 Journal Article

Semantic models for concurrent logic languages

F.S. de Boer
J.J.M.M. Rutten
J.N. Kok
C. Palamidessi

In this paper we develop semantic models for a class of concurrent logic languages. We give two operational semantics based on a transition system, a declarative semantics and a denotational semantics. One operational and the declarative semantics model the success set, that is, the set of computed answer substitutions corresponding to all successfully terminating computations. The other operational and the denotational semantics also model deadlock and infinite computations. For the declarative and the denotational semantics we extend standard notions such as unification in order to cope with the synchronization mechanism of the class of languages we study. The basic mathematical structure for the declarative semantics is the complete lattice of sets of finite streams of substitutions. In the denotational semantics, we use a complete metric space of tree-like structures that are labelled with functions that represent the basic unification step. We look at the relations between the different models. We relate first the two operational semantics and next the declarative and denotational semantics with their respective operational counterparts.

Details DOI

TCS Journal 1989 Journal Article

Declarative modeling of the operational behavior of logic languages

M. Falaschi
G. Levi
C. Palamidessi
M. Martelli

The paper defines a new declarative semantics for logic programs, which is based on interpretations containing (possibly) non-ground atoms. Two different interpretations are introduced and the corresponding models are defined and compared. The classical results on the Herbrand model semantics of logic programs are shown to hold in the new models too (i. e. existence of a minimal model, fixpoint characterization, etc.). With the new models, we have a stronger soundness and completeness result for SLD-resolution. In particular, one of the two models allows the set of computed answer substitutions to be characterized precisely.

Details DOI