Arrow Research search

Author name cluster

Raul Fervari

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.

13 papers
2 author rows

Possible papers

13

KR Conference 2025 Conference Paper

How Lucky Are You to Know Your Way? A Probabilistic Approach to Knowing How Logics

  • Pablo F. Castro
  • Pedro R. D'Argenio
  • Raul Fervari

We introduce a probabilistic version of knowing-how modal logics. More precisely, our logics extend extant approaches to model the ability of an agent to achieve a given goal with a certain probability. On the semantic side, we enrich the models of the logic with probability distributions over the agent's actions. Then, we investigate different languages to describe such structures. First, we consider a probabilistic version of the linear plan-based logic of knowing how, and discuss its properties. Then, we consider indistinguishability classes, and obtain two logics, one that has `non-adaptative' plans, and another with `adaptative' plans. In all cases we investigate the computational complexity of their model-checking problem, obtaining undecidability results for the first and the second logic, while for the last one the problem is decidable in polynomial time. We also explore the semantics of the new logics under non-probabilistic models to compare them to the original non-probabilistic ones.

PDF Details DOI

KR Conference 2025 Conference Paper

On the Effects of Adding Assignments in Linear-Time Temporal Logics Modulo Theories

  • Stéphane Demri
  • Raul Fervari

We introduce linear-time temporal logics with past operators featuring a simple assignment modality that performs local changes on the models. Such structures are infinite sequences of valuations interpreting variables by elements from a possibly infinite data domain. We study several fragments as well as the case with the Boolean domain, for which we establish that it is actually as expressive as first-order logic over infinite sequences of propositional valuations. For the logics over concrete domains N, Z and Q equipped with the respective linear ordering and equality tests, we show the satisfiability problem is decidable, and that the logics are as expressive as the version without the assignment operator. Interestingly, this entails such assignments provide a huge concise ness, which is then helpful for succinct specifications.

PDF Details DOI

AAMAS Conference 2023 Conference Paper

A Deontic Logic of Knowingly Complying

  • Carlos Areces
  • Valentin Cassano
  • Pablo F. Castro
  • Raul Fervari
  • Andrés R. Saravia

We introduce a logic for representing the deontic notion of knowingly complying –associated to an agent’s conciousness of taking a normative course of action for achieving a certain goal. Our logic features an operator for describing normative courses of actions, and another operator for describing what each agent knowingly complies with. We provide a sound and complete axiom system for our logic, and study the computational complexity of its satisfiability problem. Finally, we extend our logic with an additional operator for capturing the general abilities of the agents. This operator enables us to distinguish ‘what agents can do’ and ‘what agents do according to norms’. For this extension, we also provide a sound and complete axiom system.

PDF

JELIA Conference 2023 Conference Paper

Data Graphs with Incomplete Information (and a Way to Complete Them)

  • Carlos Areces
  • Valentin Cassano
  • Danae Dutto
  • Raul Fervari

Abstract We introduce a modal language for reasoning about data graphs with incomplete information. Such data graphs are formally represented as models in which data value functions are partial—to capture what is unknown. In this setting, we also allow for unknown data values to be learned. Our main result is a sound and strongly complete axiomatization for the logic.

Details

JELIA Conference 2023 Conference Paper

How Easy it is to Know How: An Upper Bound for the Satisfiability Problem

  • Carlos Areces
  • Valentin Cassano
  • Pablo F. Castro
  • Raul Fervari
  • Andrés R. Saravia

Abstract We investigate the complexity of the satisfiability problem for a modal logic expressing ‘knowing how’ assertions, related to an agent’s abilities to achieve a certain goal. We take one of the most standard semantics for this kind of logics based on linear plans. Our main result is a proof that checking satisfiability of a ‘knowing how’ formula can be done in \(\varSigma _2^P\). The algorithm we present relies on eliminating nested modalities in a formula, and then performing multiple calls to a satisfiability checking oracle for propositional logic.

Details

AAAI Conference 2023 Conference Paper

Model-Checking for Ability-Based Logics with Constrained Plans

  • Stéphane Demri
  • Raul Fervari

We investigate the complexity of the model-checking problem for a family of modal logics capturing the notion of “knowing how”. We consider the most standard ability-based knowing how logic, for which we show that model-checking is PSpace-complete. By contrast, a multi-agent variant based on an uncertainty relation between plans in which uncertainty is encoded by a regular language, is shown to admit a PTime model-checking problem. We extend with budgets the above-mentioned ability-logics, as done for ATL-like logics. We show that for the former logic enriched with budgets, the complexity increases to at least ExpSpace-hardness, whereas for the latter, the PTime bound is preserved. Other variant logics are discussed along the paper.

PDF Details DOI

TARK Conference 2021 Conference Paper

Uncertainty-Based Semantics for Multi-Agent Knowing How Logics

  • Carlos Areces
  • Raul Fervari
  • Andrés R. Saravia
  • Fernando R. Velázquez-Quesada

We introduce a new semantics for a multi-agent epistemic operator of knowing how, based on an indistinguishability relation between plans. Our proposal is, arguably, closer to the standard presentation of knowing that modalities in classical epistemic logic. We study the relationship between this semantics and previous approaches, showing that our setting is general enough to capture them. We also define a sound and complete axiomatization, and investigate the computational complexity of its model checking and satisfiability problems.

Details DOI

TARK Conference 2019 Conference Paper

An Algebraic Approach for Action Based Default Reasoning

  • Pablo F. Castro
  • Valentin Cassano
  • Raul Fervari
  • Carlos Areces

Often, we assume that an action is permitted simply because it is not explicitly forbidden; or, similarly, that an action is forbidden simply because it is not explicitly permitted. This kind of assumptions appear, e. g. , in autonomous computing systems where decisions must be taken in the presence of an incomplete set of norms regulating a particular scenario. Combining default and deontic reasoning over actions allows us to formally reason about such assumptions. With this in mind, we propose a logical formalism for default reasoning over a deontic action logic. The novelty of our approach is twofold. First, our formalism for default reasoning deals with actions and action operators, and it is based on the deontic action logic originally proposed by Segerberg. Second, inspired by Segerberg's approach, we use tools coming from the theory of Boolean Algebra. These tools allow us to extend Segerberg's algebraic completeness result to the setting of Default Logics.

Details DOI

JELIA Conference 2019 Conference Paper

Axiomatising Logics with Separating Conjunction and Modalities

  • Stéphane Demri
  • Raul Fervari
  • Alessio Mansutti

Abstract Modal separation logics are formalisms that combine modal operators to reason locally, with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics \(\text {MSL} ^{}(*, \langle \ne \rangle )\) and \(\text {MSL} ^{}(*, \Diamond )\), where \(*\) is the separating conjunction, \(\Diamond \) is the standard modal operator and \(\langle \ne \rangle \) is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and take advantage of new normal forms and of their axiomatisation.

Details

JELIA Conference 2019 Conference Paper

Interpolation and Beth Definability in Default Logics

  • Valentin Cassano
  • Raul Fervari
  • Carlos Areces
  • Pablo F. Castro

Abstract We investigate interpolation and Beth definability in default logics. To this end, we start by defining a general framework which is sufficiently abstract to encompass most of the usual definitions of a default logic. In this framework a default logic \(\mathscr {D}\mathfrak {L}\) is built on a base, monotonic, logic \(\mathfrak {L}\). We then investigate the question of when interpolation and Beth definability results transfer from \(\mathfrak {L}\) to \(\mathscr {D}\mathfrak {L}\). This investigation needs suitable notions of interpolation and Beth definability for default logics. We show both positive and negative general results: depending on how \(\mathscr {D}\mathfrak {L}\) is defined and of the kind of interpolation/Beth definability involved, the property might or might not transfer from \(\mathfrak {L}\) to \(\mathscr {D}\mathfrak {L}\).

Details

IJCAI Conference 2017 Conference Paper

Strategically knowing how

  • Raul Fervari
  • Andreas Herzig
  • Yanjun Li
  • Yanjing Wang

In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve phi means that there exists a (uniform) strategy such that the agent knows that it can make sure phi. We give an intuitive axiomatisation of our logic and prove the soundness, completeness, and decidability of the logic. The crucial axioms relating knowing that and knowing how illustrate our understanding of knowing how in this setting. This logic can be used in representing and reasoning about knowledge-how.

PDF Details

JELIA Conference 2016 Conference Paper

Hilbert-Style Axiomatization for Hybrid XPath with Data

  • Carlos Areces
  • Raul Fervari

Abstract In this paper we introduce a sound and complete axiomatization for XPath with data constraints extended with hybrid operators. First, we define \(\text {HXPath} _=({{\uparrow }{\downarrow }})\), an extension of vertical XPath with nominals and the hybrid operator @. Then, we introduce an axiomatic system for \(\text {HXPath} _=({{\uparrow }{\downarrow }})\), and we prove it is complete with respect to the class of abstract data trees, i. e. , data trees in which data values are abstracted as equivalence relations. As a corollary, we also obtain completeness with respect to the class of concrete data trees.

Details

GandALF Workshop 2016 Workshop Paper

Relation-Changing Logics as Fragments of Hybrid Logics

  • Carlos Areces
  • Raul Fervari
  • Guillaume Hoffmann
  • Mauricio Martel

Relation-changing modal logics are extensions of the basic modal logic that allow changes to the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add, and swap edges in the model, both locally and globally. We provide translations from these logics to hybrid logic along with an implementation. In general, these logics are undecidable, but we use our translations to identify decidable fragments. We also compare the expressive power of relation-changing modal logics with hybrid logics.

PDF Details DOI