Fundamenta Informaticae - Volume 175, issue 1-4

Authors: Jamroga, Wojciech | Konikowska, Beata | Kurpiewski, Damian | Penczek, Wojciech

Article Type: Research Article

Abstract: Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic (mv-ATL → ∗ ), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branchingtime logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. …We show that the method cannot be directly extended to mv-ATL → ∗ . We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL → ∗ . We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL → ∗ and motivate its use for model checking multi-agent systems. Show more

DOI: 10.3233/FI-2020-1955

Citation: Fundamenta Informaticae, vol. 175, no. 1-4, pp. 207-251, 2020

Authors: Janicki, Ryszard | Mikulski, Łukasz

Article Type: Research Article

Abstract: Traces and their extensions as comtraces, step traces and interval traces are quotient monoids over sequences or step sequences that play an important role in the formal analysis and verification of concurrent systems. Step traces are generalizations of comtraces and classical traces while interval traces are specialized traces that can deal with interval order semantics. The algebraic structures and their properties as projections, hidings, canonical forms and other invariants are very well established for traces and fairly well established for comtraces. For step traces and interval traces they are the main subject of this paper.

Keywords: traces, interval traces, step traces, partially commutative monoids

DOI: 10.3233/FI-2020-1956

Citation: Fundamenta Informaticae, vol. 175, no. 1-4, pp. 253-280, 2020

Authors: Sanchez Martin, Jose Angel | Petre, Ion

Article Type: Research Article

Abstract: Network controllability focuses on the concept of driving the dynamical system associated to a directed network of interactions from an arbitrary initial state to an arbitrary final state, through a well-chosen set of input functions applied in a minimal number of so-called input nodes. In earlier studies we and other groups demonstrated the potential of applying this concept in medicine. A directed network of interactions may be built around the main known drivers of the disease being studied, and then analysed to identify combinations of drug targets controlling survivability-essential genes in the network. This paper takes the next step and …focuses on patient data. We demonstrate that comprehensive protein-protein interaction networks can be built around patient genetic data, and that network controllability can be used to identify possible personalised drug combinations. We discuss the algorithmic methods that can be used to construct and analyse these networks. Show more

Keywords: Network controllability, personalised medicine, multiple myeloma, mutated genes, essential genes, drug target genes

DOI: 10.3233/FI-2020-1957

Citation: Fundamenta Informaticae, vol. 175, no. 1-4, pp. 281-299, 2020

Authors: Thiagarajan, P. S. | Yang, Shaofa

Article Type: Research Article

Abstract: We present the theory of distributed Markov chains (DMCs). A DMC consists of a collection of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key feature of a DMC is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. Using our theory of DMCs we show how one can analyze the behavior using the interleaved semantics of the model. A key point is, the transition system which defines the interleaved semantics is—except in degenerate cases—not a Markov …chain. Hence one must develop new techniques to analyze these behaviors exhibiting both concurrency and stochasticity. After establishing the core theory we develop a statistical model checking procedure which verifies the dynamical properties of the trajectories generated by the the model. The specifications consist of Boolean combinations of component-wise bounded linear time temporal logic formulas. We also provide a probabilistic Petri net representation of DMCs and use it to derive a probabilistic event structure semantics. Show more

DOI: 10.3233/FI-2020-1958

Citation: Fundamenta Informaticae, vol. 175, no. 1-4, pp. 301-325, 2020

Authors: Verbeek, Fons J. | Cao, Lu

Article Type: Research Article

Abstract: Biology is 3D. Therefore, it is important to be able to analyze phenomena in a spatiotemporal manner. Different fields in computational sciences are useful for analysis in biology; i.e. image analysis, pattern recognition and machine learning. To fit an empirical model to a higher abstraction, however, theoretical computer science methods are probed. We explore the construction of empirical 3D graphical models and develop abstractions from these models in L-systems. These systems are provided with a profound formalization in a grammar allowing generalization and exploration of mathematical structures in topologies. The connections between these computational approaches are illustrated by a …case study of the development of the lactiferous duct in mice and the phenotypical effects from different environmental conditions we can observe on it. We have constructed a workflow to get 3D models from different experimental conditions and use these models to extract features. Our aim is to construct an abstraction of these 3D models to an L-system from features that we have measured. From our measurements we can make the productions for an L-system. In this manner we can formalize the arborization of the lactiferous duct under different environmental conditions and capture different observations. All considered, this paper illustrates the joint of empirical with theoretical computational sciences and the augmentation of the interpretation of the results. At the same time, it shows a method to analyze complex 3D topologies and produces archetypes for developmental configurations. Show more

Keywords: L-system, Phenotype analysis, Center-line topology, lactiferous duct, 3D model representation

DOI: 10.3233/FI-2020-1959

Citation: Fundamenta Informaticae, vol. 175, no. 1-4, pp. 327-345, 2020