Author name cluster

Riccardo Pucella

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.

11 papers

2 author rows

TARK Conference 2017 Conference Paper

An Epistemic Foundation for Authentication Logics (Extended Abstract)

Joseph Y. Halpern
Ron van der Meyden
Riccardo Pucella

While there have been many attempts, going back to BAN logic, to base reasoning about security protocols on epistemic notions, they have not been all that successful. Arguably, this has been due to the particular logics chosen. We present a simple logic based on the well-understood modal operators of knowledge, time, and probability, and show that it is able to handle issues that have often been swept under the rug by other approaches, while being flexible enough to capture all the higher- level security notions that appear in BAN logic. Moreover, while still assuming that the knowledge operator allows for unbounded computation, it can handle the fact that a computationally bounded agent cannot decrypt messages in a natural way, by distinguishing strings and message terms. We demonstrate that our logic can capture BAN logic notions by providing a translation of the BAN operators into our logic, capturing belief by a form of probabilistic knowledge.

Details DOI

AIJ Journal 2011 Journal Article

Dealing with logical omniscience: Expressiveness and pragmatics

Joseph Y. Halpern
Riccardo Pucella

We examine four approaches for dealing with the logical omniscience problem and their potential applicability: the syntactic approach, awareness, algorithmic knowledge, and impossible possible worlds. Although in some settings these approaches are equi-expressive and can capture all epistemic states, in other settings of interest (especially with probability in the picture), we show that they are not equi-expressive. We then consider the pragmatics of dealing with logical omniscience—how to choose an approach and construct an appropriate model.

Details DOI

TARK Conference 2007 Conference Paper

Dealing with logical omniscience

Joseph Y. Halpern
Riccardo Pucella

We examine four approaches for dealing with the logical omniscience problem and their potential applicability: the syntactic approach, awareness, algorithmic knowledge, and impossible possible worlds. Although in some settings these approaches are equi-expressive and can capture all epistemic states, in other settings of interest they are not. In particular, adding probabilities to the language allows for finer distinctions between different approaches.

Details

TARK Conference 2007 Conference Paper

Perfect cryptography, S5 knowledge, and algorithmic knowledge

Sabina Petride
Riccardo Pucella

We propose a principled approach to model secrecy in multiagent systems, by defining a set of possible observations and providing agents with algorithms used to distinguish the possible states of the system. Our approach fits naturally within a knowledgebased account of secrecy. By adjusting both the kind of observations and the capabilities of the agents, we can capture in a natural way different forms of secrecy in the presence of perfect cryptography. In particular, we show how to model extraction secrecy. Our formalization suggests a unified definition of secrecy for cryptographic protocols and for systems that seek to prevent inadmissible flows of information.

Details

UAI Conference 2005 Conference Paper

Evidence with Uncertain Likelihoods

Joseph Y. Halpern
Riccardo Pucella

An agent often has a number of hypotheses, and must choose among them based on observations, or outcomes of experiments. Each of these observations can be viewed as providing evidence for or against various hypotheses. All the attempts to formalize this intuition up to now have assumed that associated with each hypothesis h there is a likelihood function μh, which is a probability measure that intuitively describes how likely each observation is, conditional on h being the correct hypothesis. We consider an extension of this framework where there is uncertainty as to which of a number of likelihood functions is appropriate, and discuss how one formal approach to defining evidence, which views evidence as a function from priors to posteriors, can be generalized to accommodate this uncertainty.

Details

TCS Journal 2004 Journal Article

A coalgebraic approach to Kleene algebra with tests

Hubie Chen
Riccardo Pucella

Kleene algebra with tests is an extension of Kleene algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene algebra with Tests, along the lines of the coalgebraic theory of regular expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene algebra with tests does not lend itself to a coalgebraic theory, we define a new interpretation of Kleene algebra with tests expressions and a corresponding automata-theoretic presentation. One outcome of the theory is a coinductive proof principle, that can be used to establish equivalence of our Kleene algebra with tests expressions.

Details DOI

UAI Conference 2003 Conference Paper

A Logic for Reasoning about Evidence

Joseph Y. Halpern
Riccardo Pucella

We introduce a logic for reasoning about evidence, that essentially views evidence as a function from prior beliefs (before making an observation) to posterior beliefs (after making the observation). We provide a sound and complete axiomatization for the logic, and consider the complexity of the decision problem. Although the reasoning in the logic is mainly propositional, we allow variables representing numbers and quantification over them. This expressive power seems necessary to capture important properties of evidence

Details

TARK Conference 2003 Conference Paper

Probabilistic algorithmic knowledge

Joseph Y. Halpern
Riccardo Pucella

The frameworkof algorithmic knowledge assumes that agents use deterministic knowledge algorithms to compute the facts they explicitly know. We extend the framework to allow for randomized knowledge algorithms. We then characterize the information provided by a randomized knowledge algorithm when its answers have some probability of being incorrect. We formalize this information in terms of evidence; a randomized knowledge algorithm returning "Yes" to a query about a fact ~oprovides evidence for qobeing true. Finally, we discuss the extent to which this evidence can be used as a basis for decisions.

Details

UAI Conference 2002 Conference Paper

Reasoning about Expectation

Joseph Y. Halpern
Riccardo Pucella

Expectation is a central notion in probability theory. The notion of expectation also makes sense for other notions of uncertainty. We introduce a propositional logic for reasoning about expectation, where the semantics depends on the underlying representation of uncertainty. We give sound and complete axiomatizations for the logic in the case that the underlying representation is (a) probability, (b) sets of probability measures, (c) belief functions, and (d) possibility measures. We show that this logic is more expressive than the corresponding logic for reasoning about likelihood in the case of sets of probability measures, but equi-expressive in the case of probability, belief, and possibility. Finally, we show that satisfiability for these logics is NP-complete, no harder than satisfiability for propositional logic.

Details

UAI Conference 2001 Conference Paper

A Logic for Reasoning about Upper Probabilities

Joseph Y. Halpern
Riccardo Pucella

We present a propositional logic to reason about the uncertainty of events, where the uncertainty is modeled by a set of probability measures assigning an interval of probability to each event. We give a sound and complete axiomatization for the logic, and show that the satisfiability problem is NP-complete, no harder than satisfiability for propositional logic.

Details

TCS Journal 2001 Journal Article

On the expressive power of first-order boolean functions in PCF

Riccardo Pucella
Prakash Panangaden

Recent results of Bucciarelli show that the semilattice of degrees of parallelism of first-order boolean functions in PCF has both infinite chains and infinite antichains. By considering a simple subclass of Sieber's sequentiality relations, we identify levels in the semilattice and derive inexpressibility results concerning functions on different levels. This allows us to further explore the structure of the semilattice of degrees of parallelism: we identify semilattices characterized by simple level properties, and show the existence of new infinite hierarchies which are in a certain sense natural with respect to the levels.

Details DOI