-
A proof theoretic basis for relational semantics
Authors:
Carlos G. Lopez Pombo,
Thomas S. E. Maibaum
Abstract:
Logic has proved essential for formally modeling software based systems. Such formal descriptions, frequently called specifications, have served not only as requirements documentation and formalisation, but also for providing the mathematical foundations for their analysis and the development of automated reasoning tools.
Logic is usually studied in terms of its two inherent aspects: syntax and…
▽ More
Logic has proved essential for formally modeling software based systems. Such formal descriptions, frequently called specifications, have served not only as requirements documentation and formalisation, but also for providing the mathematical foundations for their analysis and the development of automated reasoning tools.
Logic is usually studied in terms of its two inherent aspects: syntax and semantics. The relevance of the latter resides in the fact that producing logical descriptions of real-world phenomena, requires people to agree on how such descriptions are to be interpreted and understood by human beings, so that systems can be built with confidence in accordance with their specification. On the more practical side, the metalogical relation between syntax and semantics, determines important aspects of the conclusions one can draw from the application of certain analysis techniques, like model checking.
Abstract model theory (i.e., the mathematical perspective on semantics of logical languages) is of little practical value to software engineering endeavours. From our point of view, values (those that can be assigned to constants and variables) should not be just points in a platonic domain of interpretation, but elements that can be named by means of terms over the signature of the specification. In a nutshell, we are not interested in properties that require any semantic information not representable using the available syntax.
In this paper we present a framework supporting the proof theoretical formalisation of classes of relational models for behavioural logical languages, whose domains of discourse are guaranteed to be formed exclusively by nameable values.
△ Less
Submitted 17 July, 2021;
originally announced July 2021.
-
On the construction of explosive relation algebras
Authors:
Carlos G. Lopez Pombo,
Marcelo F. Frias,
Thomas S. E. Maibaum
Abstract:
Fork algebras are an extension of relation algebras obtained by extending the set of logical symbols with a binary operator called fork. This class of algebras was introduced by Haeberer and Veloso in the early 90's aiming at enriching relation algebra, an already successful language for program specification, with the capability of expressing some form of parallel computation.
The further study…
▽ More
Fork algebras are an extension of relation algebras obtained by extending the set of logical symbols with a binary operator called fork. This class of algebras was introduced by Haeberer and Veloso in the early 90's aiming at enriching relation algebra, an already successful language for program specification, with the capability of expressing some form of parallel computation.
The further study of this class of algebras led to many meaningful results linked to interesting properties of relation algebras such as representability and finite axiomatizability, among others. Also in the 90's, Veloso introduced a subclass of relation algebras that are expansible to fork algebras, admitting a large number of non-isomorphic expansions, referred to as explosive relation algebras.
In this work we discuss some general techniques for constructing algebras of this type.
△ Less
Submitted 9 September, 2020; v1 submitted 6 September, 2020;
originally announced September 2020.
-
Actions and Events in Concurrent Systems Design
Authors:
Valentin Cassano,
Thomas S. E. Maibaum
Abstract:
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…
▽ More
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.
△ Less
Submitted 5 January, 2014;
originally announced January 2014.
-
Automated Reasoning over Deontic Action Logics with Finite Vocabularies
Authors:
Pablo F. Castro,
Thomas S. E. Maibaum
Abstract:
In this paper we investigate further the tableaux system for a deontic action logic we presented in previous work. This tableaux system uses atoms (of a given boolean algebra of action terms) as labels of formulae, this allows us to embrace parallel execution of actions and action complement, two action operators that may present difficulties in their treatment. One of the restrictions of this lo…
▽ More
In this paper we investigate further the tableaux system for a deontic action logic we presented in previous work. This tableaux system uses atoms (of a given boolean algebra of action terms) as labels of formulae, this allows us to embrace parallel execution of actions and action complement, two action operators that may present difficulties in their treatment. One of the restrictions of this logic is that it uses vocabularies with a finite number of actions. In this article we prove that this restriction does not affect the coherence of the deduction system; in other words, we prove that the system is complete with respect to language extension. We also study the computational complexity of this extended deductive framework and we prove that the complexity of this system is in PSPACE, which is an improvement with respect to related systems.
△ Less
Submitted 5 January, 2014;
originally announced January 2014.
