-
Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs
Authors:
Maris F. L. Galesloot,
Roman Andriushchenko,
Milan Češka,
Sebastian Junges,
Nils Jansen
Abstract:
Partially observable Markov decision processes (POMDPs) model specific environments in sequential decision-making under uncertainty. Critically, optimal policies for POMDPs may not be robust against perturbations in the environment. Hidden-model POMDPs (HM-POMDPs) capture sets of different environment models, that is, POMDPs with a shared action and observation space. The intuition is that the tru…
▽ More
Partially observable Markov decision processes (POMDPs) model specific environments in sequential decision-making under uncertainty. Critically, optimal policies for POMDPs may not be robust against perturbations in the environment. Hidden-model POMDPs (HM-POMDPs) capture sets of different environment models, that is, POMDPs with a shared action and observation space. The intuition is that the true model is hidden among a set of potential models, and it is unknown which model will be the environment at execution time. A policy is robust for a given HM-POMDP if it achieves sufficient performance for each of its POMDPs.We compute such robust policies by combining two orthogonal techniques: (1) a deductive formal verification technique that supports tractable robust policy evaluation by computing a worst-case POMDP within the HM-POMDP, and (2) subgradient ascent to optimize the candidate policy for a worst-case POMDP. The empirical evaluation shows that, compared to various baselines, our approach (1) produces policies that are more robust and generalize better to unseen POMDPs, and (2) scales to HM-POMDPs that consist of over a hundred thousand environments.
△ Less
Submitted 20 June, 2025; v1 submitted 14 May, 2025;
originally announced May 2025.
-
Decentralized Planning Using Probabilistic Hyperproperties
Authors:
Francesco Pontiggia,
Filip Macák,
Roman Andriushchenko,
Michele Chiari,
Milan Češka
Abstract:
Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set…
▽ More
Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set of decentralized agents operating in the environment. We extend existing approaches for model checking probabilistic hyperproperties to handle temporal formulae relating paths of different agents, thus requiring the self-composition between multiple MDPs. Using several case studies, we demonstrate that our approach provides a flexible and expressive framework to broaden the specification capabilities with respect to existing planning techniques. Additionally, we establish a close connection between a subclass of probabilistic hyperproperties and planning for a particular type of Dec-MDPs, for both of which we show undecidability. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.
△ Less
Submitted 19 February, 2025;
originally announced February 2025.
-
Small Decision Trees for MDPs with Deductive Synthesis
Authors:
Roman Andriushchenko,
Milan Češka,
Sebastian Junges,
Filip Macák
Abstract:
Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can efficiently compute policies that are optimal with respect to, e.g., reachability probabilities. However, these policies are then given in a tabular format. A longstanding challenge is to represent optimal or almost-optimal…
▽ More
Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can efficiently compute policies that are optimal with respect to, e.g., reachability probabilities. However, these policies are then given in a tabular format. A longstanding challenge is to represent optimal or almost-optimal policies concisely, e.g., as decision trees. This paper makes two contributions towards this challenge: first, an SMT-based approach to encode a given (optimal) policy as a small decision tree, and second, an abstraction-refinement loop that searches for policies that are optimal within the set of policies that can be represented with a small tree. Technically, the latter combines the SMT encoding with verification approaches for families of Markov chains. The empirical evaluation demonstrates the feasibility of these approaches and shows how they can outperform the state-of-the-art on various benchmarks, yielding up to 20 times smaller trees representing (almost) optimal policies for models with up to 10k states and 19 variables.
△ Less
Submitted 22 May, 2025; v1 submitted 17 January, 2025;
originally announced January 2025.
-
Policies Grow on Trees: Model Checking Families of MDPs
Authors:
Roman Andriushchenko,
Milan Češka,
Sebastian Junges,
Filip Macák
Abstract:
Markov decision processes (MDPs) provide a fundamental model for sequential decision making under process uncertainty. A classical synthesis task is to compute for a given MDP a winning policy that achieves a desired specification. However, at design time, one typically needs to consider a family of MDPs modelling various system variations. For a given family, we study synthesising (1) the subset…
▽ More
Markov decision processes (MDPs) provide a fundamental model for sequential decision making under process uncertainty. A classical synthesis task is to compute for a given MDP a winning policy that achieves a desired specification. However, at design time, one typically needs to consider a family of MDPs modelling various system variations. For a given family, we study synthesising (1) the subset of MDPs where a winning policy exists and (2) a preferably small number of winning policies that together cover this subset. We introduce policy trees that concisely capture the synthesis result. The key ingredient for synthesising policy trees is a recursive application of a game-based abstraction. We combine this abstraction with an efficient refinement procedure and a post-processing step. An extensive empirical evaluation demonstrates superior scalability of our approach compared to naive baselines. For one of the benchmarks, we find 246 winning policies covering 94 million MDPs. Our algorithm requires less than 30 minutes, whereas the naive baseline only covers 3.7% of MDPs in 24 hours.
△ Less
Submitted 17 July, 2024;
originally announced July 2024.
-
Tools at the Frontiers of Quantitative Verification
Authors:
Roman Andriushchenko,
Alexander Bork,
Carlos E. Budde,
Milan Češka,
Kush Grover,
Ernst Moritz Hahn,
Arnd Hartmanns,
Bryant Israelsen,
Nils Jansen,
Joshua Jeppson,
Sebastian Junges,
Maximilian A. Köhl,
Bettina Könighofer,
Jan Křetínský,
Tobias Meggendorfer,
David Parker,
Stefan Pranger,
Tim Quatmann,
Enno Ruijters,
Landon Taylor,
Matthias Volk,
Maximilian Weininger,
Zhen Zhang
Abstract:
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused o…
▽ More
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.
△ Less
Submitted 22 May, 2024;
originally announced May 2024.
-
Deductive Controller Synthesis for Probabilistic Hyperproperties
Authors:
Roman Andriushchenko,
Ezio Bartocci,
Milan Ceska,
Francesco Pontiggia,
Sarah Sallinger
Abstract:
Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and…
▽ More
Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. Our specification language builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach considerably outperforms HyperProb, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g. partial observability) as well as inter-controller constraints (e.g. agreements on a common action).
△ Less
Submitted 10 July, 2023;
originally announced July 2023.
-
Search and Explore: Symbiotic Policy Synthesis in POMDPs
Authors:
Roman Andriushchenko,
Alexander Bork,
Milan Češka,
Sebastian Junges,
Joost-Pieter Katoen,
Filip Macák
Abstract:
This paper marries two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making under uncertainty. A central issue is to find a POMDP controller - that solely decides based on the observations seen so far - to achieve a total expected reward objective. As finding optimal controllers is undecidable, we…
▽ More
This paper marries two state-of-the-art controller synthesis methods for partially observable Markov decision processes (POMDPs), a prominent model in sequential decision making under uncertainty. A central issue is to find a POMDP controller - that solely decides based on the observations seen so far - to achieve a total expected reward objective. As finding optimal controllers is undecidable, we concentrate on synthesising good finite-state controllers (FSCs). We do so by tightly integrating two modern, orthogonal methods for POMDP controller synthesis: a belief-based and an inductive approach. The former method obtains an FSC from a finite fragment of the so-called belief MDP, an MDP that keeps track of the probabilities of equally observable POMDP states. The latter is an inductive search technique over a set of FSCs, e.g., controllers with a fixed memory size. The key result of this paper is a symbiotic anytime algorithm that tightly integrates both approaches such that each profits from the controllers constructed by the other. Experimental results indicate a substantial improvement in the value of the controllers while significantly reducing the synthesis time and memory footprint.
△ Less
Submitted 29 May, 2023; v1 submitted 23 May, 2023;
originally announced May 2023.
-
Designing Approximate Arithmetic Circuits with Combined Error Constraints
Authors:
Milan Češka,
Jiří Matyáš,
Vojtech Mrazek,
Tomáš Vojnar
Abstract:
Approximate circuits trading the power consumption for the quality of results play a key role in the development of energy-aware systems. Designing complex approximate circuits is, however, a very difficult and computationally demanding process. When deploying approximate circuits, various error metrics (e.g., mean average error, worst-case error, error rate), as well as other constraints (e.g., c…
▽ More
Approximate circuits trading the power consumption for the quality of results play a key role in the development of energy-aware systems. Designing complex approximate circuits is, however, a very difficult and computationally demanding process. When deploying approximate circuits, various error metrics (e.g., mean average error, worst-case error, error rate), as well as other constraints (e.g., correct multiplication by 0), have to be considered. The state-of-the-art approximation methods typically focus on a single metric which significantly limits the applicability of the resulting circuits. In this paper, we experimentally investigate how various error metrics and their combinations affect the reduction of the power consumption that can be achieved. To this end, we extend evolutionary-driven techniques that allow us to effectively explore the design space of the approximate circuits. We identify principal limitations when complex error constraints are required as well as important correlations among the error metrics enabling the construction of circuits providing the best-known trade-offs between the power reduction and combined error constraints.
△ Less
Submitted 27 June, 2022;
originally announced June 2022.
-
Abstraction-Based Segmental Simulation of Chemical Reaction Networks
Authors:
Martin Helfrich,
Milan Češka,
Jan Křetínský,
Štefan Martiček
Abstract:
Simulating chemical reaction networks is often computationally demanding, in particular due to stiffness. We propose a novel simulation scheme where long runs are not simulated as a whole but assembled from shorter precomputed segments of simulation runs. On the one hand, this speeds up the simulation process to obtain multiple runs since we can reuse the segments. On the other hand, questions on…
▽ More
Simulating chemical reaction networks is often computationally demanding, in particular due to stiffness. We propose a novel simulation scheme where long runs are not simulated as a whole but assembled from shorter precomputed segments of simulation runs. On the one hand, this speeds up the simulation process to obtain multiple runs since we can reuse the segments. On the other hand, questions on diversity and genuineness of our runs arise. However, we ensure that we generate runs close to their true distribution by generating an appropriate abstraction of the original system and utilizing it in the simulation process. Interestingly, as a by-product, we also obtain a yet more efficient simulation scheme, yielding runs over the system's abstraction. These provide a very faithful approximation of concrete runs on the desired level of granularity, at a low cost. Our experiments demonstrate the speedups in the simulations while preserving key dynamical as well as quantitative properties.
△ Less
Submitted 18 June, 2022; v1 submitted 14 June, 2022;
originally announced June 2022.
-
Inductive Synthesis of Finite-State Controllers for POMDPs
Authors:
Roman Andriushchenko,
Milan Ceska,
Sebastian Junges,
Joost-Pieter Katoen
Abstract:
We present a novel learning framework to obtain finite-state controllers (FSCs) for partially observable Markov decision processes and illustrate its applicability for indefinite-horizon specifications. Our framework builds on oracle-guided inductive synthesis to explore a design space compactly representing available FSCs. The inductive synthesis approach consists of two stages: The outer stage d…
▽ More
We present a novel learning framework to obtain finite-state controllers (FSCs) for partially observable Markov decision processes and illustrate its applicability for indefinite-horizon specifications. Our framework builds on oracle-guided inductive synthesis to explore a design space compactly representing available FSCs. The inductive synthesis approach consists of two stages: The outer stage determines the design space, i.e., the set of FSC candidates, while the inner stage efficiently explores the design space. This framework is easily generalisable and shows promising results when compared to existing approaches. Experiments indicate that our technique is (i) competitive to state-of-the-art belief-based approaches for indefinite-horizon properties, (ii) yields smaller FSCs than existing methods for several models, and (iii) naturally treats multi-objective specifications.
△ Less
Submitted 22 March, 2022; v1 submitted 21 March, 2022;
originally announced March 2022.
-
Model Repair Revamped: On the Automated Synthesis of Markov Chains
Authors:
Milan Ceska,
Christian Dehnert,
Nils Jansen,
Sebastian Junges,
Joost-Pieter Katoen
Abstract:
This paper outlines two approaches|based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verifica…
▽ More
This paper outlines two approaches|based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input. We show the applicability of these synthesis techniques to sketching of probabilistic programs, controller synthesis of POMDPs, and software product lines.
△ Less
Submitted 27 May, 2021;
originally announced May 2021.
-
Inductive Synthesis for Probabilistic Programs Reaches New Horizons
Authors:
Roman Andriushchenko,
Milan Ceska,
Sebastian Junges,
Joost-Pieter Katoen
Abstract:
This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a PCTL specification. The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the famil…
▽ More
This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a PCTL specification. The method builds on a novel inductive oracle that greedily generates counter-examples (CEs) for violating programs and uses them to prune the family. These CEs leverage the semantics of the family in the form of bounds on its best- and worst-case behaviour provided by a deductive oracle using an MDP abstraction. The method further monitors the performance of the synthesis and adaptively switches between the inductive and deductive reasoning. Our experiments demonstrate that the novel CE construction provides a significantly faster and more effective pruning strategy leading to acceleration of the synthesis process on a wide range of benchmarks. For challenging problems, such as the synthesis of decentralized partially-observable controllers, we reduce the run-time from a day to minutes.
△ Less
Submitted 29 January, 2021;
originally announced January 2021.
-
Adaptive Verifiability-Driven Strategy for Evolutionary Approximation of Arithmetic Circuits
Authors:
Milan Ceska,
Jiri Matyas,
Vojtech Mrazek,
Lukas Sekanina,
Zdenek Vasicek,
Tomas Vojnar
Abstract:
We present a novel approach for designing complex approximate arithmetic circuits that trade correctness for power consumption and play important role in many energy-aware applications. Our approach integrates in a unique way formal methods providing formal guarantees on the approximation error into an evolutionary circuit optimisation algorithm. The key idea is to employ a novel adaptive search s…
▽ More
We present a novel approach for designing complex approximate arithmetic circuits that trade correctness for power consumption and play important role in many energy-aware applications. Our approach integrates in a unique way formal methods providing formal guarantees on the approximation error into an evolutionary circuit optimisation algorithm. The key idea is to employ a novel adaptive search strategy that drives the evolution towards promptly verifiable approximate circuits. As demonstrated in an extensive experimental evaluation including several structurally different arithmetic circuits and target precisions, the search strategy provides superior scalability and versatility with respect to various approximation scenarios. Our approach significantly improves capabilities of the existing methods and paves a way towards an automated design process of provably-correct circuit approximations.
△ Less
Submitted 5 March, 2020;
originally announced March 2020.
-
Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks
Authors:
Milan Češka,
Jan Křetínský
Abstract:
Analysis of large continuous-time stochastic systems is a computationally intensive task. In this work we focus on population models arising from chemical reaction networks (CRNs), which play a fundamental role in analysis and design of biochemical systems. Many relevant CRNs are particularly challenging for existing techniques due to complex dynamics including stochasticity, stiffness or multimod…
▽ More
Analysis of large continuous-time stochastic systems is a computationally intensive task. In this work we focus on population models arising from chemical reaction networks (CRNs), which play a fundamental role in analysis and design of biochemical systems. Many relevant CRNs are particularly challenging for existing techniques due to complex dynamics including stochasticity, stiffness or multimodal population distributions. We propose a novel approach allowing not only to predict, but also to explain both the transient and steady-state behaviour. It focuses on qualitative description of the behaviour and aims at quantitative precision only in orders of magnitude. Firstly, we abstract the CRN into a compact model preserving rough timing information, distinguishing only signifcinatly different populations, but capturing relevant sequences of behaviour. Secondly, we approximately analyse the most probable temporal behaviours of the model through most probable transitions. As demonstrated on complex CRNs from literature, our approach reproduces the known results, but in contrast to the state-of-the-art methods, it runs with virtually no computational cost and thus offers unprecedented~scalability.
△ Less
Submitted 23 May, 2019;
originally announced May 2019.
-
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Authors:
Milan Češka,
Christian Hensel,
Sebastian Junges,
Joost-Pieter Katoen
Abstract:
Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our a…
▽ More
Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.
△ Less
Submitted 28 April, 2019;
originally announced April 2019.
-
Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata
Authors:
Milan Češka,
Vojtěch Havlena,
Lukáš Holík,
Jan Kořenek,
Ondřej Lengál,
Denis Matoušek,
Jiří Matoušek,
Jakub Semrič,
Tomáš Vojnar
Abstract:
Deep packet inspection via regular expression (RE) matching is a crucial task of network intrusion detection systems (IDSes), which secure Internet connection against attacks and suspicious network traffic. Monitoring high-speed computer networks (100 Gbps and faster) in a single-box solution demands that the RE matching, traditionally based on finite automata (FAs), is accelerated in hardware. In…
▽ More
Deep packet inspection via regular expression (RE) matching is a crucial task of network intrusion detection systems (IDSes), which secure Internet connection against attacks and suspicious network traffic. Monitoring high-speed computer networks (100 Gbps and faster) in a single-box solution demands that the RE matching, traditionally based on finite automata (FAs), is accelerated in hardware. In this paper, we describe a novel FPGA architecture for RE matching that is able to process network traffic beyond 100 Gbps. The key idea is to reduce the required FPGA resources by leveraging approximate nondeterministic FAs (NFAs). The NFAs are compiled into a multi-stage architecture starting with the least precise stage with a high throughput and ending with the most precise stage with a low throughput. To obtain the reduced NFAs, we propose new approximate reduction techniques that take into account the profile of the network traffic. Our experiments showed that using our approach, we were able to perform matching of large sets of REs from SNORT, a popular IDS, on unprecedented network speeds.
△ Less
Submitted 24 April, 2019;
originally announced April 2019.
-
Shepherding Hordes of Markov Chains
Authors:
Milan Ceska,
Nils Jansen,
Sebastian Junges,
Joost-Pieter Katoen
Abstract:
This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, planning under partial observability, and sketching of probabilistic programs. Simple questions, like `does at least one family member satisfy a property?', are NP-hard. We tackle two problems: distinguish family members t…
▽ More
This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, planning under partial observability, and sketching of probabilistic programs. Simple questions, like `does at least one family member satisfy a property?', are NP-hard. We tackle two problems: distinguish family members that satisfy a given quantitative property from those that do not, and determine a family member that satisfies the property optimally, i.e., with the highest probability or reward. We show that combining two well-known techniques, MDP model checking and abstraction refinement, mitigates the computational complexity. Experiments on a broad set of benchmarks show that in many situations, our approach is able to handle families of millions of MCs, providing superior scalability compared to existing solutions.
△ Less
Submitted 26 March, 2019; v1 submitted 15 February, 2019;
originally announced February 2019.
-
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection (Technical Report)
Authors:
Milan Ceska,
Vojtech Havlena,
Lukas Holik,
Ondrej Lengal,
Tomas Vojnar
Abstract:
We consider the problem of approximate reduction of non-deterministic automata that appear in hardware-accelerated network intrusion detection systems (NIDSes). We define an error distance of a reduced automaton from the original one as the probability of packets being incorrectly classified by the reduced automaton (wrt the probabilistic distribution of packets in the network traffic). We use thi…
▽ More
We consider the problem of approximate reduction of non-deterministic automata that appear in hardware-accelerated network intrusion detection systems (NIDSes). We define an error distance of a reduced automaton from the original one as the probability of packets being incorrectly classified by the reduced automaton (wrt the probabilistic distribution of packets in the network traffic). We use this notion to design an approximate reduction procedure that achieves a great size reduction (much beyond the state-of-the-art language-preserving techniques) with a controlled and small error. We have implemented our approach and evaluated it on use cases from Snort, a popular NIDS. Our results provide experimental evidence that the method can be highly efficient in practice, allowing NIDSes to follow the rapid growth in the speed of networks.
△ Less
Submitted 21 February, 2018; v1 submitted 24 October, 2017;
originally announced October 2017.
-
On Robustness Analysis of Stochastic Biochemical Systems by Probabilistic Model Checking
Authors:
Lubos Brim,
Milan Ceska,
Sven Drazan,
David Safranek
Abstract:
This report proposes a novel framework for a rigorous robustness analysis of stochastic biochemical systems. The technique is based on probabilistic model checking. We adapt the general definition of robustness introduced by Kitano to the class of stochastic systems modelled as continuous time Markov Chains in order to extensively analyse and compare robustness of biological models with uncertain…
▽ More
This report proposes a novel framework for a rigorous robustness analysis of stochastic biochemical systems. The technique is based on probabilistic model checking. We adapt the general definition of robustness introduced by Kitano to the class of stochastic systems modelled as continuous time Markov Chains in order to extensively analyse and compare robustness of biological models with uncertain parameters. The framework utilises novel computational methods that enable to effectively evaluate the robustness of models with respect to quantitative temporal properties and parameters such as reaction rate constants and initial conditions.
The framework is applied to gene regulation as an example of a central biological mechanism where intrinsic and extrinsic stochasticity plays crucial role due to low numbers of DNA and RNA molecules. Using our methods we have obtained a comprehensive and precise analysis of stochastic dynamics under parameter uncertainty. Furthermore, we apply our framework to compare several variants of two-component signalling networks from the perspective of robustness with respect to intrinsic noise caused by low populations of signalling components. We succeeded to extend previous studies performed on deterministic models (ODE) and show that stochasticity may significantly affect obtained predictions. Our case studies demonstrate that the framework can provide deeper insight into the role of key parameters in maintaining the system functionality and thus it significantly contributes to formal methods in computational systems biology.
△ Less
Submitted 17 October, 2013;
originally announced October 2013.
-
Computing Optimal Cycle Mean in Parallel on CUDA
Authors:
Jiří Barnat,
Petr Bauch,
Luboš Brim,
Milan Češka
Abstract:
Computation of optimal cycle mean in a directed weighted graph has many applications in program analysis, performance verification in particular. In this paper we propose a data-parallel algorithmic solution to the problem and show how the computation of optimal cycle mean can be efficiently accelerated by means of CUDA technology. We show how the problem of computation of optimal cycle mean is de…
▽ More
Computation of optimal cycle mean in a directed weighted graph has many applications in program analysis, performance verification in particular. In this paper we propose a data-parallel algorithmic solution to the problem and show how the computation of optimal cycle mean can be efficiently accelerated by means of CUDA technology. We show how the problem of computation of optimal cycle mean is decomposed into a sequence of data-parallel graph computation primitives and show how these primitives can be implemented and optimized for CUDA computation. Finally, we report a fivefold experimental speed up on graphs representing models of distributed systems when compared to best sequential algorithms.
△ Less
Submitted 1 November, 2011;
originally announced November 2011.
-
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking
Authors:
Jiří Barnat,
Luboš Brim,
Milan Češka
Abstract:
In this paper we present a tool that performs CUDA accelerated LTL Model Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA architecture in order to efficiently detect the presence of accepting cycles in a directed graph. Accepting cycle detection is the core algorithmic procedure in automata-based LTL Model Checking. We demonstrate that the tool outperforms non-accel…
▽ More
In this paper we present a tool that performs CUDA accelerated LTL Model Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA architecture in order to efficiently detect the presence of accepting cycles in a directed graph. Accepting cycle detection is the core algorithmic procedure in automata-based LTL Model Checking. We demonstrate that the tool outperforms non-accelerated version of the algorithm and we discuss where the limits of the tool are and what we intend to do in the future to avoid them.
△ Less
Submitted 13 December, 2009;
originally announced December 2009.
