-
Annotating Control-Flow Graphs for Formalized Test Coverage Criteria
Authors:
Sean Kauffman,
Carlos Moreno,
Sebastian Fischmeister
Abstract:
Control flow coverage criteria are an important part of the process of qualifying embedded software for safety-critical systems. Criteria such as modified condition/decision coverage (MC/DC) as defined by DO-178B are used by regulators to judge the adequacy of testing and by QA engineers to design tests when full path coverage is impossible.
Despite their importance, these coverage criteria are…
▽ More
Control flow coverage criteria are an important part of the process of qualifying embedded software for safety-critical systems. Criteria such as modified condition/decision coverage (MC/DC) as defined by DO-178B are used by regulators to judge the adequacy of testing and by QA engineers to design tests when full path coverage is impossible.
Despite their importance, these coverage criteria are often misunderstood. One problem is that their definitions are typically written in natural language specification documents, making them imprecise. Other works have proposed formal definitions using binary predicate logic, but these definitions are difficult to apply to the analysis of real programs. Control-Flow Graphs (CFGs) are the most common model for analyzing program logic in compilers, and seem to be a good fit for defining and analyzing coverage criteria. However, CFGs discard the explicit concept of a decision, making their use for this task seem impossible.
In this paper, we show how to annotate a CFG with decision information inferred from the graph itself. We call this annotated model a Control-Flow Decision Graph (CFDG) and we use it to formally define several common coverage criteria. We have implemented our algorithms in a tool which we show can be applied to automatically annotate CFGs output from popular compilers.
△ Less
Submitted 4 July, 2024;
originally announced July 2024.
-
The Complexity of Data-Free Nfer
Authors:
Sean Kauffman,
Kim Guldstrand Larsen,
Martin Zimmermann
Abstract:
Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input…
▽ More
Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input exists that will generate a given interval. By excluding data from the language, we obtain polynomial-time algorithms for the evaluation problem and for satisfiability when only considering inclusive rules. Furthermore, we show decidability for the satisfiability problem for cycle-free specifications and undecidability for satisfiability of full data-free nfer.
△ Less
Submitted 3 July, 2024;
originally announced July 2024.
-
The Hiatus Between Organism and Machine Evolution: Contrasting Mixed Microbial Communities with Robots
Authors:
Andrea Roli,
Stuart A. Kauffman
Abstract:
Mixed microbial communities, usually composed of various bacterial and fungal species, are fundamental in a plethora of environments, from soil to human gut and skin. Their evolution is a paradigmatic example of intertwined dynamics, where not just the relations among species plays a role, but also the opportunities -- and possible harms -- that each species presents to the others. These opportuni…
▽ More
Mixed microbial communities, usually composed of various bacterial and fungal species, are fundamental in a plethora of environments, from soil to human gut and skin. Their evolution is a paradigmatic example of intertwined dynamics, where not just the relations among species plays a role, but also the opportunities -- and possible harms -- that each species presents to the others. These opportunities are in fact \textit{affordances}, which can be seized by heritable variation and selection. In this paper, starting from a systemic viewpoint of mixed microbial communities, we focus on the pivotal role of affordances in evolution and we contrast it to the artificial evolution of programs and robots. We maintain that the two realms are neatly separated, in that natural evolution proceeds by extending the space of its possibilities in a completely open way, while the latter is inherently limited by the algorithmic framework it is defined. This discrepancy characterises also an envisioned setting in which robots evolve in the physical world. We present arguments supporting our claim and we propose an experimental setting for assessing our statements. Rather than just discussing the limitations of the artificial evolution of machines, the aim of this contribution is to emphasize the tremendous potential of the evolution of the biosphere, beautifully represented by the evolution of communities of microbes.
△ Less
Submitted 29 June, 2022;
originally announced June 2022.
-
Monitoring Timed Properties (Revisited)
Authors:
Thomas Møller Grosen,
Sean Kauffman,
Kim Guldstrand Larsen,
Martin Zimmermann
Abstract:
In this paper we revisit monitoring real-time systems with respect to properties expressed either in Metric Interval Temporal Logic or as Timed Büchi Automata. We offer efficient symbolic online monitoring algorithms in a number of settings, exploiting so-called zones well-known from efficient model checking of Timed Automata. The settings considered include new, much simplified treatment of time…
▽ More
In this paper we revisit monitoring real-time systems with respect to properties expressed either in Metric Interval Temporal Logic or as Timed Büchi Automata. We offer efficient symbolic online monitoring algorithms in a number of settings, exploiting so-called zones well-known from efficient model checking of Timed Automata. The settings considered include new, much simplified treatment of time divergence, monitoring under timing uncertainty, and extension of monitoring to offer minimum time estimates before conclusive verdicts can be made.
△ Less
Submitted 5 September, 2022; v1 submitted 29 June, 2022;
originally announced June 2022.
-
The Complexity of Evaluating nfer
Authors:
Sean Kauffman,
Martin Zimmermann
Abstract:
Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules.
We show that the…
▽ More
Nfer is a rule-based language for abstracting event streams into a hierarchy of intervals with data. Nfer has multiple implementations and has been applied in the analysis of spacecraft telemetry and autonomous vehicle logs. This work provides the first complexity analysis of nfer evaluation, i.e., the problem of deciding whether a given interval is generated by applying rules.
We show that the full nfer language is undecidable and that this depends on both recursion in the rules and an infinite data domain. By restricting either or both of those capabilities, we obtain tight decidability results. We also examine the impact on complexity of exclusive rules and minimality. For the most practical case, which is minimality with finite data, we provide a polynomial-time algorithm.
△ Less
Submitted 21 November, 2022; v1 submitted 28 February, 2022;
originally announced February 2022.
-
What Is Consciousness? Artificial Intelligence, Real Intelligence, Quantum Mind, And Qualia
Authors:
Stuart A. Kauffman,
Andrea Roli
Abstract:
We approach the question "What is Consciousness?" in a new way, not as Descartes' "systematic doubt", but as how organisms find their way in their world. Finding one's way involves finding possible uses of features of the world that might be beneficial or avoiding those that might be harmful. "Possible uses of X to accomplish Y" are "Affordances". The number of uses of X is indefinite (or unknown)…
▽ More
We approach the question "What is Consciousness?" in a new way, not as Descartes' "systematic doubt", but as how organisms find their way in their world. Finding one's way involves finding possible uses of features of the world that might be beneficial or avoiding those that might be harmful. "Possible uses of X to accomplish Y" are "Affordances". The number of uses of X is indefinite (or unknown), the different uses are unordered, are not listable, and are not deducible from one another. All biological adaptations are either affordances seized by heritable variation and selection or, far faster, by the organism acting in its world finding uses of X to accomplish Y. Based on this, we reach rather astonishing conclusions: (1) Artificial general intelligence based on universal Turing machines (UTMs) is not possible, since UTMs cannot "find" novel affordances. (2) Brain-mind is not purely classical physics for no classical physics system can be an analogue computer whose dynamical behaviour can be isomorphic to "possible uses". (3) Brain mind must be partly quantum-supported by increasing evidence at 6.0 sigma to 7.3 sigma. (4) Based on Heisenberg's interpretation of the quantum state as "potentia" converted to "actuals" by measurement, where this interpretation is not a substance dualism, a natural hypothesis is that mind actualizes potentia. This is supported at 5.2 sigma. Then mind's actualizations of entangled brain-mind-world states are experienced as qualia and allow "seeing" or "perceiving" of uses of X to accomplish Y. We can and do jury-rig. Computers cannot. (5) Beyond familiar quantum computers, we discuss the potentialities of trans-Turing-systems.
△ Less
Submitted 29 June, 2022; v1 submitted 12 April, 2021;
originally announced June 2021.
-
Online adaptation in robots as biological development provides phenotypic plasticity
Authors:
Michele Braccini,
Andrea Roli,
Stuart A. Kauffman
Abstract:
The ability of responding to environmental stimuli with appropriate actions is a property shared by all living organisms, and it is also sought in the design of robotic systems. Phenotypic plasticity provides a way for achieving this property as it characterises those organisms that, from one genotype, can express different phenotypes in response to different environments, without involving geneti…
▽ More
The ability of responding to environmental stimuli with appropriate actions is a property shared by all living organisms, and it is also sought in the design of robotic systems. Phenotypic plasticity provides a way for achieving this property as it characterises those organisms that, from one genotype, can express different phenotypes in response to different environments, without involving genetic modifications. In this work we study phenotypic plasticity in robots that are equipped with online sensor adaptation. We show that Boolean network controlled robots can attain navigation with collision avoidance by adapting the coupling between proximity sensors and their controlling network without changing its structure. In other terms, these robots, while being characterised by one genotype (i.e. the network) can express a phenotype among many that is suited for the specific environment. We also show that the dynamical regime that makes it possible to attain the best overall performance is the critical one, bringing further evidence to the hypothesis that natural and artificial systems capable of optimally balancing robustness and adaptivity are critical.
△ Less
Submitted 3 June, 2020;
originally announced June 2020.
-
Self-referential basis of undecidable dynamics: from The Liar Paradox and The Halting Problem to The Edge of Chaos
Authors:
Mikhail Prokopenko,
Michael Harré,
Joseph Lizier,
Fabio Boschetti,
Pavlos Peppas,
Stuart Kauffman
Abstract:
In this paper we explore several fundamental relations between formal systems, algorithms, and dynamical systems, focussing on the roles of undecidability, universality, diagonalization, and self-reference in each of these computational frameworks. Some of these interconnections are well-known, while some are clarified in this study as a result of a fine-grained comparison between recursive formal…
▽ More
In this paper we explore several fundamental relations between formal systems, algorithms, and dynamical systems, focussing on the roles of undecidability, universality, diagonalization, and self-reference in each of these computational frameworks. Some of these interconnections are well-known, while some are clarified in this study as a result of a fine-grained comparison between recursive formal systems, Turing machines, and Cellular Automata (CAs). In particular, we elaborate on the diagonalization argument applied to distributed computation carried out by CAs, illustrating the key elements of Gödel's proof for CAs. The comparative analysis emphasizes three factors which underlie the capacity to generate undecidable dynamics within the examined computational frameworks: (i) the program-data duality; (ii) the potential to access an infinite computational medium; and (iii) the ability to implement negation. The considered adaptations of Gödel's proof distinguish between computational universality and undecidability, and show how the diagonalization argument exploits, on several levels, the self-referential basis of undecidability.
△ Less
Submitted 20 March, 2019; v1 submitted 7 November, 2017;
originally announced November 2017.
-
The Role of Redundancy in the Robustness of Random Boolean Networks
Authors:
Carlos Gershenson,
Stuart A. Kauffman,
Ilya Shmulevich
Abstract:
Evolution depends on the possibility of successfully exploring fitness landscapes via mutation and recombination. With these search procedures, exploration is difficult in "rugged" fitness landscapes, where small mutations can drastically change functionalities in an organism. Random Boolean networks (RBNs), being general models, can be used to explore theories of how evolution can take place in…
▽ More
Evolution depends on the possibility of successfully exploring fitness landscapes via mutation and recombination. With these search procedures, exploration is difficult in "rugged" fitness landscapes, where small mutations can drastically change functionalities in an organism. Random Boolean networks (RBNs), being general models, can be used to explore theories of how evolution can take place in rugged landscapes; or even change the landscapes.
In this paper, we study the effect that redundant nodes have on the robustness of RBNs. Using computer simulations, we have found that the addition of redundant nodes to RBNs increases their robustness. We conjecture that redundancy is a way of "smoothening" fitness landscapes. Therefore, redundancy can facilitate evolutionary searches. However, too much redundancy could reduce the rate of adaptation of an evolutionary process. Our results also provide supporting evidence in favour of Kauffman's conjecture (Kauffman, 2000, p.195).
△ Less
Submitted 11 January, 2006; v1 submitted 9 November, 2005;
originally announced November 2005.