A Lewisian approach to the verification of adaptive systems

Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

Many software artifacts like software architectures or distributed programs are characterized by a high level of
dynamism involving changes in their structure or behaviour as a response to external stimuli or as the result of
programmed reconfigurations. When reasoning on such adaptive systems one is not only interested in proving
properties on their global behaviour like system correctness, but also on the evolution of the single components. For instance, when analysing the well-known stable marriage problem one would like to know whether a solution ensures that “two females never claim to be married with the same male”. To enable automatic reasoning, two main things are needed: models for the software artifacts and logic-based languages for describing their properties. One of the most successful and versatile model for such artifacts are graphs. Regarding the property specification languages, variants of quantified temporal logics have been proposed, which combine the modal operators of temporal logics with monadic second-order logic for graphs. Unfortunately, the semantical models for such logics are not clearly cut, due to the possibility to interleave modal operators and quantifiers in formulae like $x.◊ψ where x is quantified in a world but ψ states properties about x in a reachable world or state where it does not necessarily exist or even have the same identity. The issue is denoted in the quantified temporal logic
literature as trans-world identity [1, 3]. A typical solution follows the so-called “Kripke semantics” approach: roughly, a set of universal items is chosen, and its elements are used to form each state. This solution is the most widely adopted, and it underlines all the proposals we are aware of Kripke-like solutions do not fit well with the merging, deletion and creation of components, neither allows for an easy inclusion of evolution relations possibly forming cycles: if the value of an open formula is a set of states, how to account e.g. for an element that is first deleted and then added again? This problem is often solved by restricting the class of admissible evolution relations: this forces to reformulate the state transition relation modeling the system evolution, hampering the intuitive meaning of the logic. In [2, 5] we presented an alternative approach, inspired to counterpart theory [4]. The key point of Lewis's proposal is the notion of counterpart, which is a consequence of his refusal to interpret the relation of trans-world sameness as
strict identity. In our approach we exploit counterpart relations, i.e. (partial) functions among states, explicitly relating elements of different states. Our solution avoids some limitations of the existing approaches, in particular in what regards the treatment of the possible merging and reuse of components. Moreover, the resulting semantics is a streamlined and intuitively appealing one, yet it is general enough to cover most of the alternatives we are aware of.
Original languageEnglish
JournalRivista Italiana di Filosofia Analitica Junior
Volume2
Issue number2
ISSN2037-4445
Publication statusPublished - 2011
Externally publishedYes

Fingerprint Dive into the research topics of 'A Lewisian approach to the verification of adaptive systems'. Together they form a unique fingerprint.

Cite this