Valentin Cassano

Carlos Areces, Pablo Barceló, Valentin Cassano et al.

We study the satisfiability problem for a modal logic expressing knowing-how assertions, which captures an agent's ability to achieve a given goal under the standard semantics based on linear plans. Our main result shows that satisfiability of knowing-how formulas is NP-complete, improving previously known complexity bounds. The proof proceeds via a translation into modal logic S5, an instrumental tool for addressing a variety of problems in knowledge representation.

Valentin Cassano, Thomas S. E. Maibaum

In this work, having in mind the construction of concurrent systems from components, we discuss the difference between actions and events. For this discussion, we propose an(other) architecture description language in which actions and events are made explicit in the description of a component and a system. Our work builds from the ideas set forth by the categorical approach to the construction of software based systems from components advocated by Goguen and Burstall, in the context of institutions, and by Fiadeiro and Maibaum, in the context of temporal logic. In this context, we formalize a notion of a component as an element of an indexed category and we elicit a notion of a morphism between components as morphisms of this category. Moreover, we elaborate on how this formalization captures, in a convenient manner, the underlying structure of a component and the basic interaction mechanisms for putting components together. Further, we advance some ideas on how certain matters related to the openness and the compositionality of a component/system may be described in terms of classes of morphisms, thus potentially supporting a compositional rely/guarantee reasoning.