-
Paraconsistent Transition Systems
Authors:
Ana Cruz,
Alexandre Madeira,
LuÂ-Ã-s Soares Barbosa
Abstract:
Often in Software Engineering, a modeling formalism has to support scenarios of inconsistency in which several requirements either reinforce or contradict each other. Paraconsistent transition systems are proposed in this paper as one such formalism: states evolve through two accessibility relations capturing weighted evidence of a transition or its absence, respectively. Their weights come from a…
▽ More
Often in Software Engineering, a modeling formalism has to support scenarios of inconsistency in which several requirements either reinforce or contradict each other. Paraconsistent transition systems are proposed in this paper as one such formalism: states evolve through two accessibility relations capturing weighted evidence of a transition or its absence, respectively. Their weights come from a specific residuated lattice. A category of these systems, and the corresponding algebra, is defined as providing a formal setting to model different application scenarios. One of them, dealing with the effect of quantum decoherence in quantum programs, is used for illustration purposes.
△ Less
Submitted 23 March, 2023;
originally announced March 2023.
-
The Economics of the DeLend Project: Agent-based Simulations
Authors:
Frederico Dutilh Novaes,
Gabriel de Abreu Madeira,
Aurimar Cerqueira
Abstract:
This paper presents our methodology to simulate the behavior of the DeLend Platform. Such simulations are important to verify if the system is able to connect the different sets of agents linked to the platform in a functional manner. They also provide inputs to guide the choices of operational parameters, such as the platform spread, and strategies by DeLend, since they estimate how the key varia…
▽ More
This paper presents our methodology to simulate the behavior of the DeLend Platform. Such simulations are important to verify if the system is able to connect the different sets of agents linked to the platform in a functional manner. They also provide inputs to guide the choices of operational parameters, such as the platform spread, and strategies by DeLend, since they estimate how the key variables of interest respond to different policies. We discuss the methodology and provide examples meant to clarify the approach and to how we intend to use the tool in practice -- they should not be interpreted as representative of real life scenarios.
△ Less
Submitted 2 April, 2023; v1 submitted 6 March, 2023;
originally announced March 2023.
-
A Logic for Paraconsistent Transition Systems
Authors:
Ana Cruz,
Alexandre Madeira,
Luís Soares Barbosa
Abstract:
Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. In this kind of scenarios, arising e.g. in knowledge representation, simulation of biological systems, or quantum computation, inconsistency has to be addressed in a precise and controlled way. This paper generalises Belna…
▽ More
Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. In this kind of scenarios, arising e.g. in knowledge representation, simulation of biological systems, or quantum computation, inconsistency has to be addressed in a precise and controlled way. This paper generalises Belnap-Dunn four-valued logic, introducing paraconsistent transition systems (PTS), endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values, and their modal logic.
△ Less
Submitted 13 April, 2022;
originally announced April 2022.
-
Generalising KAT to verify weighted computations
Authors:
Leandro Gomes,
Alexandre Madeira,
Luís Soares Barbosa
Abstract:
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests…
▽ More
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). On this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT [22], we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M(n,A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.
△ Less
Submitted 4 November, 2019;
originally announced November 2019.
-
A Hybrid Dynamic Logic for Event/Data-based Systems
Authors:
Rolf Hennicker,
Alexandre Madeira,
Alexander Knapp
Abstract:
We propose $\mathcal{E}^{\downarrow}$-logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic act…
▽ More
We propose $\mathcal{E}^{\downarrow}$-logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs $e /ψ$ where $e$ is an event and $ψ$ a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that $\mathcal{E}^{\downarrow}$-logic is powerful enough to characterise the semantics of an operational specification by a single $\mathcal{E}^{\downarrow}$-sentence. Thus the whole development process can rely on $\mathcal{E}^{\downarrow}$-logic and its semantics as a common basis. This includes also a variety of implementation constructors to support, among others, event refinement and parallel composition.
△ Less
Submitted 8 February, 2019;
originally announced February 2019.
-
Asymmetric combination of logics is functorial: A survey
Authors:
Renato Neves,
Alexandre Madeira,
Luis S. Barbosa,
Manuel A. Martins
Abstract:
Asymmetric combination of logics is a formal process that develops the characteristic features of a specific logic on top of another one. Typical examples include the development of temporal, hybrid, and probabilistic dimensions over a given base logic. These examples are surveyed in the paper under a particular perspective - that this sort of combination of logics possesses a functorial nature. S…
▽ More
Asymmetric combination of logics is a formal process that develops the characteristic features of a specific logic on top of another one. Typical examples include the development of temporal, hybrid, and probabilistic dimensions over a given base logic. These examples are surveyed in the paper under a particular perspective - that this sort of combination of logics possesses a functorial nature. Such a view gives rise to several interesting questions. They range from the problem of combining translations (between logics), to that of ensuring property preservation along the process, and the way different asymmetric combinations can be related through appropriate natural transformations.
△ Less
Submitted 8 May, 2017; v1 submitted 13 November, 2016;
originally announced November 2016.
-
A logic for n-dimensional hierarchical refinement
Authors:
Alexandre Madeira,
Manuel A. Martins,
Luís S. Barbosa
Abstract:
Hierarchical transition systems provide a popular mathematical structure to represent state-based software applications in which different layers of abstraction are represented by inter-related state machines. The decomposition of high level states into inner sub-states, and of their transitions into inner sub-transitions is common refinement procedure adopted in a number of specification formalis…
▽ More
Hierarchical transition systems provide a popular mathematical structure to represent state-based software applications in which different layers of abstraction are represented by inter-related state machines. The decomposition of high level states into inner sub-states, and of their transitions into inner sub-transitions is common refinement procedure adopted in a number of specification formalisms.
This paper introduces a hybrid modal logic for k-layered transition systems, its first-order standard translation, a notion of bisimulation, and a modal invariance result. Layered and hierarchical notions of refinement are also discussed in this setting.
△ Less
Submitted 7 June, 2016;
originally announced June 2016.
-
The role of logical interpretations in program development
Authors:
Manuel A. Martins,
Alexandre Madeira,
Luis S. Barbosa
Abstract:
Stepwise refinement of algebraic specifications is a well known formal methodology for program development. However, traditional notions of refinement based on signature morphisms are often too rigid to capture a number of relevant transformations in the context of software design, reuse, and adaptation. This paper proposes a new approach to refinement in which signature morphisms are replaced by…
▽ More
Stepwise refinement of algebraic specifications is a well known formal methodology for program development. However, traditional notions of refinement based on signature morphisms are often too rigid to capture a number of relevant transformations in the context of software design, reuse, and adaptation. This paper proposes a new approach to refinement in which signature morphisms are replaced by logical interpretations as a means to witness refinements. The approach is first presented in the context of equational logic, and later generalised to deductive systems of arbitrary dimension. This allows, for example, refining sentential into equational specifications and the latter into modal ones.
△ Less
Submitted 29 January, 2014; v1 submitted 27 November, 2013;
originally announced November 2013.
-
Bisimilarity and refinement for hybrid(ised) logics
Authors:
Alexandre Madeira,
Manuel A. Martins,
Luís Soares Barbosa
Abstract:
The complexity of modern software systems entails the need for reconfiguration mechanisms gov- erning the dynamic evolution of their execution configurations in response to both external stimulus or internal performance measures. Formally, such systems may be represented by transition systems whose nodes correspond to the different configurations they may assume. Therefore, each node is en- dowed…
▽ More
The complexity of modern software systems entails the need for reconfiguration mechanisms gov- erning the dynamic evolution of their execution configurations in response to both external stimulus or internal performance measures. Formally, such systems may be represented by transition systems whose nodes correspond to the different configurations they may assume. Therefore, each node is en- dowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of this sort of systems. Therefore, the quest for suitable notions of equivalence and refinement between models of hybrid logic specifications becomes fundamental to any design discipline adopting this perspective. This paper contributes to this effort from a distinctive point of view: instead of focussing on a specific hybrid logic, the paper introduces notions of bisimilarity and refinement for hybridised logics, i.e. standard specification logics (e.g. propositional, equational, fuzzy, etc) to which modal and hybrid features were added in a systematic way.
△ Less
Submitted 27 May, 2013;
originally announced May 2013.
-
Refinement by interpretation in π-institutions
Authors:
César Rodrigues,
Manuel A. Martins,
Alexandre Madeira,
Luis S. Barbosa
Abstract:
The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of pi-institutions. This leads to a smooth generalization of the refinement-by-interpretation approach, recently introduced by the authors in more specific contexts. As a second, yet related contribution a basis is provided to b…
▽ More
The paper discusses the role of interpretations, understood as multifunctions that preserve and reflect logical consequence, as refinement witnesses in the general setting of pi-institutions. This leads to a smooth generalization of the refinement-by-interpretation approach, recently introduced by the authors in more specific contexts. As a second, yet related contribution a basis is provided to build up a refinement calculus of structured specifications in and across arbitrary pi-institutions.
△ Less
Submitted 21 June, 2011;
originally announced June 2011.
