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. In this presentation we 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. The material presented in this talk was recently published in [CMB22].
[CMB22]A logic for paraconsistent transition systems A. Cruz, A. Madeira and L. Barbosa. Non-Classic Logics. Theory and Applications. EPTCS (in print)
Leandro Gomes, INESC TEC, U. MINHO, Portugal
Semantics and dynamic logics for fuzzy programs
(joint work with Alexandre Madeira and Luís Soares Barbosa)
This work presents a framework to formally reason about weighted compu- tations or, more precisely, programs and assertions about them whose execution or evaluation has some form of weight associated. By weight we mean a value which may represent, for example, an uncertainty in the execution, or a quan- tity of resources consumed, such as energy or time. Examples of such systems range from device-to-device communications, network biological processes, clin- ical decision support systems or robot control, having become ubiquitous in our everyday life in the past years. Due to the complexity underlying the introduc- tion of these parameters, software engineering is forced to call upon rigorous development methodologies which provide a high assurance of each software product. And if it is true that the development, analysis and verification of these systems are increasingly laid on this exactly approach, the current pro- gramming practices are not capable to offer a framework which is, at the same time, generic enough to capture such paradigms, and able to satisfy the specific requirements for each application domain.
We intend to address this challenge by presenting a methodology for the systematic development of semantics and logics to reason about two distinct classes of programs. In the first class, that we call single-flow computation, each execution is a single transition with an associated weight. In the second class, that we call multi-flow computation, each execution may assume multi- ple simultaneous execution paths, each one of them with a, possible distinct, weight. In this work we define, for each class of computation, a semantics, and we prove that it forms a suitable algebra to reason about programs of that class. For that end, we define operators which interpret the basic constructions of an imperative programming language: sequential composition, conditionals and iteration. From here we construct (a family of) dynamic logics, including the respective axiomatic system, allowing to verify properties over those programs.
For single-flow computations, we define as well a notion of bisimilarity on the models of the generated logics, and prove the modal invariance property for those logics.
[Koz97] Dexter Kozen. Kleene algebra with tests. ACM Transactions on Pro- gramming Languages and Systems, 19(3):427–443, 1997.
[Gog67] J.A Goguen. L-fuzzy sets. Journal of Mathematical Analysis and Applications, 18(1):145 – 174, 1967.
[MNM16] Alexandre Madeira, Renato Neves, and Manuel A. Martins. An ex- ercise on the generation of many-valued dynamic logics. Journal of Logical and Algebraic Methods in Programming, 85(5):1011–1037, 2016.
[FKST17] Hitoshi Furusawa, Yasuo Kawahara, Georg Struth, and Norihiro Tsumagari. Kleisli, Parikh and Peleg compositions and liftings for multirela- tions. Journal of Logical and Algebraic Methods in Programming, 90:84–101, 2017.
[VMA10] Thom as Vetterlein, Harald Mandl, and Klaus-Peter Adlassnig. Fuzzy Arden syntax: A fuzzy programming language for medicine. Artificial Intel- ligence in Medicine, 49(1):1 – 10, 2010.