MEALS Dissemination Event - Abstract
Invited speaker
| Andreas Herzig (IRIT, FR) Title: Knowledge and action: how should we combine their logics? |
| Abstract: The design of logical systems accounting for both knowledge and action is an important issue in AI and MAS. While there are fairly well-established logics of knowledge---essentially the modal logics S5 and S4.2---, there is much less consensus about logical formalisms for actions: there exists a plethora of rather expressive formal systems, including situation calculus, event calculus, fluent calculus, and dynamic logic. When one combines these formal systems with epistemic logic then one typically supposes that knowledge and actions are related through the principles of perfect recall and no miracles. The resulting many-dimensional logics often have high complexity or are undecidable. In this talk I will advocate a combination that is based on a simple account of action: a dialect of Propositional Dynamic Logic PDL whose atomic programs are assignments of propositional variables. Its epistemic extension generalises the notion of visibility of a propositional variable by an agent, as proposed by van der Hoek, Wooldridge and colleagues. The model checking, satisfiability and validity problems of the resulting logic are all PSPACE complete. The logic allows to capture in a natural way several concepts that were studied in the literature, including logics of propositional control and epistemic boolean games. |
Workshop speakers
| Álvaro Torralba (Saar, GER) Title: Task Irrelevance Pruning in AI Planning |
| Abstract: In this talk we'll briefly introduce the problem of cost-optimal planning and how state of the art planners use heuristic search to solve it. Then, we'll talk about how to automatically simplify planning tasks prior to the search by removing some parts that are irrelevant. |
| Sergio Abriola (UBA, AR) Title: Model Theory of XPath |
| Abstract: We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over data trees. We show definability theorems and separation theorems for pointed data trees and node expressions. We define the notion of binary bisimulation, and we show definability and separation theorems with respect to classes of two-pointed data trees and in the context of path expressions. We also show other results and current research topics from our work in XPath, such as complete axiomatizations of some fragments of the logic. |
| Guido Chari (UBA, AR) Title: Towards Fully Reflective Environments |
| Abstract: Modern development environments promote live programming (LP) mechanisms because it enhances the development experience by providing instantaneous feedback and interaction with live objects. LP is typically supported with advanced reflective techniques within dynamic languages. These languages run on top of Virtual Machines (VMs) that are built in a static manner so that most of their components are bound at compile time. As a consequence, VM developers are forced to work using the traditional edit-compile-run cycle. We explore the idea of bringing LP techniques to VM development to improve the observability, evolution and adaptability of VMs at run-time. Our first experiments also show the opportunities such reflective capabilities provide for unanticipated dynamic adaptation scenarios, benefiting thus, a wider range of users. |
| Pablo Castro (UNRC, AR) Title: Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications |
| Abstract: We will present our approach to the problem of synthesizing fault- tolerant components from specifications, i.e., the problem of automatically constructing a fault-tolerant component implementation from a logical specification of the component, and the system’s required level of fault-tolerance. We study a specific level of fault-tolerance: masking tolerance. A system exhibits masking tolerance when both the liveness and the safety properties of the behaviors of the system are preserved under the occurrence of faults. In our approach, the logical specification of components is given in dCTL, a branching time temporal logic with deontic operators, especially designed for fault-tolerant component specification. The synthesis algorithm takes the component specification, and automatically determines whether a component with masking fault-tolerance is realizable. |
| Facundo Bustos (UNC, AR) Title: Optimizing Planning Domains by Automatic Action Schema Splitting |
| Abstract: In this work, we automate a transformation technique from a planning task to another planning task, such it preserves the solutions set and furthermore reduces the number of grounded actions exponentially, which we hope that produces an improvement of the planner's runtime. Thus, we can use the second planning task as alternative of the first with the goal to find a solution to the original planning task. The technique consists basically in split the parametrized actions (with big interfaces) into several subactions (with smaller interfaces). This involves a trade-off between interface size and plan length, which we explore by designing automatic domain optimization methods. Our experiments show that this technique could substantially improve planner's performance. |
| Juan Pablo Galeotti (UBA, AR) Title: Towards an Evolutionary Approach to Unit-Level Invariant Discovery |
| Abstract: Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes. |
| Renzo Degiovanni (UNRC, AR) Title: Specifying Event-Based Systems with a Counting Fluent Temporal Logic |
| Abstract: Fluent linear temporal logic is a formalism for specifying properties of event-based systems, based on propositions called fluents, defined in terms of activating and deactivating events. In this talk, we'll present a Counting Fluent temporal logic that complements the notion of fluent by the related concept of counting fluent. As opposed to the boolean nature of fluents, counting fluents are numerical values, that enumerate event occurrences, and allow us to specify naturally some properties of reactive systems. Although by extending fluent linear temporal logic with counting fluents we obtain an undecidable, strictly more expressive formalism, we develop a sound (but incomplete) model checking approach for the logic, that reduces to traditional temporal logic model checking, and allows us to automatically analyse properties involving counting fluents, on finite event-based systems. Our experimental evaluation show that: (i) counting fluent temporal logic is better suited than traditional temporal logic for expressing properties in which the number of occurrences of certain events is relevant, and (ii) our model checking approach on counting fluent specifications is more efficient and scales better than model checking equivalent fluent temporal logic specifications. |
| Matías David Lee (UNC, AR) Title: SOS rule formats for convex and abstract probabilistic bisimulations |
| Abstract: Probabilistic transition system specifications (PTSSs) in the ntμfθ/ntμxθ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence for all operator defined in such format. Starting from the ntμfθ/ntμxθ, we obtain restricted formats that guarantee that three coarser bisimulation equivalences are congruences. We focus on (i) Segala’s variant of bisimulation that considers combined transitions, which we call here convex bisimulation; (ii) the bisimulation equivalence resulting from considering Park & Milner’s bisimulation on the usual stripped probabilistic transition system (translated into a labelled transition system), which we call here probability obliterated bisimulation; and (iii) a probability abstracted bisimulation, which, like bisimulation, preserves the structure of the distributions but instead, it ignores the probability values. In addition, we compare these bisimulation equivalences and provide a logic characterization for each of them. |
