-
Chapter and Conference Paper
Phenotype Control of Partially Specified Boolean Networks
Partially specified Boolean networks (PSBNs) represent a promising framework for the qualitative modelling of biological systems in which the logic of interactions is not completely known. Phenotype control ai...
-
Article
Open AccessExploring attractor bifurcations in Boolean networks
Boolean networks (BNs) provide an effective modelling formalism for various complex biochemical phenomena. Their long term behaviour is represented by attractors–subsets of the state space towards which the BN...
-
Chapter and Conference Paper
Aeon 2021: Bifurcation Decision Trees in Boolean Networks
Aeon is a recent tool which enables efficient analysis of long-term behaviour of asynchronous Boolean networks with unknown parameters. In this tool paper, we present a novel major release of Aeon (Aeon 2021) ...
-
Chapter and Conference Paper
Symbolic Coloured SCC Decomposition
Problems arising in many scientific disciplines are often modelled using edge-coloured directed graphs. These can be enormous in the number of both vertices and colours. Given such a graph, the original proble...
-
Chapter and Conference Paper
Computing Bottom SCCs Symbolically Using Transition Guided Reduction
Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamica...
-
Chapter and Conference Paper
AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks
Boolean networks (BNs) provide an effective modelling tool for various phenomena from science and engineering. Any long-term behaviour of a BN eventually converges to a so-called attractor. Depending on variou...
-
Chapter and Conference Paper
Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks
Boolean networks offer an elegant way to model the behaviour of complex systems with positive and negative feedback. The long-term behaviour of a Boolean network is characterised by its attractors. Depending o...
-
Chapter and Conference Paper
Accelerating Parameter Synthesis Using Semi-algebraic Constraints
We propose a novel approach to parameter synthesis for parametrised Kripke structures and CTL specifications. In our method, we suppose the parametrisations form a semi-algebraic set and we utilise a symbolic ...
-
Chapter
Model Checking Approach to the Analysis of Biological Systems
Formal verification techniques together with other computer science formal methods have been recently tailored for applications to biological and biomedical systems. In contrast to traditional simulation-based...
-
Chapter and Conference Paper
Digital Bifurcation Analysis of TCP Dynamics
Digital bifurcation analysis is a new algorithmic method for exploring how the behaviour of a parameter-dependent computer system varies with a change in its parameters and, in particular, for identification o...
-
Chapter and Conference Paper
Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such co...
-
Chapter and Conference Paper
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems
We present a novel tool for parameter synthesis of piecewise multi-affine dynamical systems from specifications expressed in a hybrid branching-time temporal logic. The tool is based on the algorithm of parall...
-
Chapter and Conference Paper
Detecting Attractors in Biological Models with Uncertain Parameters
Complex behaviour arising in biological systems is typically characterised by various kinds of attractors. An important problem in this area is to determine these attractors. Biological systems are usually des...
-
Article
Analysing sanity of requirements for avionics systems
In the last decade it became a common practice to formalise software requirements to improve the clarity of users’ expectations. In this work we build on the fact that functional requirements can be expressed ...
-
Chapter and Conference Paper
Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems
We propose a novel scalable parallel algorithm for synthesis of interdependent parameters from CTL specifications for non-linear dynamical systems. The method employs a symbolic representation of sets of param...
-
Chapter and Conference Paper
Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis
The motivation for this study comes from various sources such as parametric formal verification, requirements engineering, and safety analysis. In these areas, there are often situations in which we are given ...
-
Chapter and Conference Paper
High-Performance Symbolic Parameter Synthesis of Biological Models: A Case Study
Complex behaviour arising in biological systems is described by highly parameterised dynamical models. Most of the parameters are mutually dependent and therefore it is hard and computationally demanding to fi...
-
Chapter and Conference Paper
A Model Checking Approach to Discrete Bifurcation Analysis
Bifurcation analysis is a central task of the analysis of parameterised high-dimensional dynamical systems that undergo transitions as parameters are changed. The classical numerical and analytical methods are...
-
Chapter and Conference Paper
LTL Parameter Synthesis of Parametric Timed Automata
The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which...
-
Article
Refinement checking on parametric modal transition systems
Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently k...
