Fundamenta Informaticae - Volume 173, issue 2-3

Authors: Kleijn, Jetty | Leuştean, Laurenţiu | Lucanu, Dorel

Article Type: Other

DOI: 10.3233/FI-2020-1917

Citation: Fundamenta Informaticae, vol. 173, no. 2-3, pp. i-ii, 2020

Authors: Sofronie-Stokkermans, Viorica

Article Type: Research Article

Abstract: In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We analyze the possibility of automatically generating such guarantees in the form of constraints on parameters. We illustrate our methods on several examples.

DOI: 10.3233/FI-2020-1918

Citation: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 91-138, 2020

Authors: Paduraru, Ciprian Ionut | Stefanescu, Gheorghe

Article Type: Research Article

Abstract: The relation between a structure and the function it runs is of interest in many fields, including computer science, biology (organ vs. function) and psychology (body vs. mind). Our paper addresses this question with reference to computer science recent hardware and software advances, particularly in areas as Robotics, Self-Adaptive Systems, IoT, CPS, AI-Hardware, etc. At the modelling, conceptual level our main contribution is the introduction of the concept of “virtual organism” (VO), to populate the intermediary level between reconfigurable hardware agents and intelligent, adaptive software agents. A virtual organism has a structure, resembling the hardware capabilities, and it runs …low-level functions, implementing the software requirements. The model is compositional in space (allowing the virtual organisms to aggregate into larger organisms) and in time (allowing the virtual organisms to get composed functionalities). The virtual organisms studied here are in 2D (two dimensions) and their structures are described by 2D patterns (adding time, we get a 3D model). By reconfiguration an organism may change its structure to another structure in the same 2D pattern. We illustrate the VO concept with a few increasingly more complex VO’s dealing with flow management or a publisher-subscriber mechanism for handling services. We implemented a simulator for a VO, collecting flow over a tree-structure (TC-VO), and the quantitative results show reconfigurable structures are better suited than fixed structures in dynamically changing environments. Finally, we briefly show how Agapia - a structured parallel, interactive programming language where dataflow and control flow structures can be freely mixed - may be used for getting quick implementations for VO’s simulation. Show more

Keywords: Distributed programming languages, Self-organizing autonomic computing, Heterogeneous (hybrid) systems, Hardware-software binding, 2D regular expressions, Agapia programming

DOI: 10.3233/FI-2020-1919

Citation: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 139-176, 2020

Authors: Diaconescu, Denisa

Article Type: Research Article

Abstract: In this paper we investigate the Hennessy-Milner property for models of many-valued modal logics defined based on complete MTL-chains having many-valued accessibility relations. Our main result gives a necessary and sufficient algebraic condition for the class of image-finite models for such modal logics to admit the Hennessy-Milner property.

Keywords: many-valued logics, modal logics, bisimulation, Hennessy-Milner property

DOI: 10.3233/FI-2020-1920

Citation: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 177-189, 2020

Authors: Leuştean, Ioana | Moangă, Natalia | Şerbănuţă, Traian Florin

Article Type: Research Article

Abstract: We propose a general system that combines the powerful features of modal logic and many-sorted reasoning. Its algebraic semantics leads to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the Jónsson-Tarski theorem. Our goal was to deepen the connections between modal logic and program verification, while also testing the expressiveness of our system by defining a small imperative language and its operational semantics.

Keywords: Polyadic modal logic, many-sorted logic, boolean algebras with operators, many-sorted algebras, Jónsson-Tarski theorem, operational semantics

DOI: 10.3233/FI-2020-1921

Citation: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 191-215, 2020

Authors: Caltais, Georgiana | Mousavi, Mohammad Reza | Singh, Hargurbir

Article Type: Research Article

Abstract: Determining and computing root causes in system failures is a significant issue in science and engineering. In this paper, we introduce a notion of causality for explaining counterexamples in system analysis based on formal models. The counter-examples are produced by checking for hazardous situations expressed in the Hennessy-Milner Logic, in the context of Labelled Transition System models. We also introduce CauseJMu, a tool for automatically identifying such causal computations within a system model. CauseJMu relies on encoding causality in terms of an extension of Hennessy-Milner Logic to recursive formulae with data. The encodings enable deciding whether a certain computation is …causal or not, using the mCRL2 model checker. Show more

Keywords: Cauality, Counterfactual causal reasoning, Concurrency, Labelled Transition Systems, Hennessy Milner Logic, Safety, Model-checking, Process algebra, mCRL2

DOI: 10.3233/FI-2020-1922

Citation: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 217-251, 2020