@inproceedings{1421, abstract = {Hybridization methods enable the analysis of hybrid automata with complex, nonlinear dynamics through a sound abstraction process. Complex dynamics are converted to simpler ones with added noise, and then analysis is done using a reachability method for the simpler dynamics. Several such recent approaches advocate that only "dynamic" hybridization techniquesi.e., those where the dynamics are abstracted on-The-fly during a reachability computation are effective. In this paper, we demonstrate this is not the case, and create static hybridization methods that are more scalable than earlier approaches. The main insight in our approach is that quick, numeric simulations can be used to guide the process, eliminating the need for an exponential number of hybridization domains. Transitions between domains are generally timetriggered, avoiding accumulated error from geometric intersections. We enhance our static technique by combining time-Triggered transitions with occasional space-Triggered transitions, and demonstrate the benefits of the combined approach in what we call mixed-Triggered hybridization. Finally, error modes are inserted to confirm that the reachable states stay within the hybridized regions. The developed techniques can scale to higher dimensions than previous static approaches, while enabling the parallelization of the main performance bottleneck for many dynamic hybridization approaches: The nonlinear optimization required for sound dynamics abstraction. We implement our method as a model transformation pass in the HYST tool, and perform reachability analysis and evaluation using an unmodified version of SpaceEx on nonlinear models with up to six dimensions.}, author = {Bak, Stanley and Bogomolov, Sergiy and Henzinger, Thomas A and Johnson, Taylor and Prakash, Pradyot}, location = {Vienna, Austria}, pages = {155 -- 164}, publisher = {Springer}, title = {{Scalable static hybridization methods for analysis of nonlinear systems}}, doi = {10.1145/2883817.2883837}, year = {2016}, } @inproceedings{1439, abstract = {Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.}, author = {Dragoi, Cezara and Henzinger, Thomas A and Zufferey, Damien}, location = {St. Petersburg, FL, USA}, pages = {400 -- 415}, publisher = {ACM}, title = {{PSYNC: A partially synchronous language for fault-tolerant distributed algorithms}}, doi = {10.1145/2837614.2837650}, volume = {20-22}, year = {2016}, } @inproceedings{1524, abstract = {When designing genetic circuits, the typical primitives used in major existing modelling formalisms are gene interaction graphs, where edges between genes denote either an activation or inhibition relation. However, when designing experiments, it is important to be precise about the low-level mechanistic details as to how each such relation is implemented. The rule-based modelling language Kappa allows to unambiguously specify mechanistic details such as DNA binding sites, dimerisation of transcription factors, or co-operative interactions. Such a detailed description comes with complexity and computationally costly executions. We propose a general method for automatically transforming a rule-based program, by eliminating intermediate species and adjusting the rate constants accordingly. To the best of our knowledge, we show the first automated reduction of rule-based models based on equilibrium approximations. Our algorithm is an adaptation of an existing algorithm, which was designed for reducing reaction-based programs; our version of the algorithm scans the rule-based Kappa model in search for those interaction patterns known to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional checks are then performed in order to verify if the reduction is meaningful in the context of the full model. The reduced model is efficiently obtained by static inspection over the rule-set. The tool is tested on a detailed rule-based model of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has 11 rules and 5 agents, and provides a dramatic reduction in simulation time of several orders of magnitude.}, author = {Beica, Andreea and Guet, Calin C and Petrov, Tatjana}, location = {Madrid, Spain}, pages = {173 -- 191}, publisher = {Springer}, title = {{Efficient reduction of kappa models by static inspection of the rule-set}}, doi = {10.1007/978-3-319-26916-0_10}, volume = {9271}, year = {2016}, } @inproceedings{1526, abstract = {We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of uncertain inputs and formalize their robustness using the analytic notion of Lipschitz continuity: a timed I/O system is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions over timed words such as the timed version of the Manhattan distance and the Skorokhod distance. We consider two models of timed I/O systems — timed transducers and asynchronous sequential circuits. We show that K-robustness of timed transducers can be decided in polynomial space under certain conditions. For asynchronous sequential circuits, we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete letter-to-letter transducers and show PSpace-completeness of the problem.}, author = {Henzinger, Thomas A and Otop, Jan and Samanta, Roopsha}, location = {St. Petersburg, FL, USA}, pages = {250 -- 267}, publisher = {Springer}, title = {{Lipschitz robustness of timed I/O systems}}, doi = {10.1007/978-3-662-49122-5_12}, volume = {9583}, year = {2016}, } @article{1148, abstract = {Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space. © 2016 Elsevier Ireland Ltd}, author = {Schilling, Christian and Bogomolov, Sergiy and Henzinger, Thomas A and Podelski, Andreas and Ruess, Jakob}, journal = {Biosystems}, pages = {15 -- 25}, publisher = {Elsevier}, title = {{Adaptive moment closure for parameter inference of biochemical reaction networks}}, doi = {10.1016/j.biosystems.2016.07.005}, volume = {149}, year = {2016}, } @article{1705, abstract = {Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based on coarse-grained space abstractions for guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.}, author = {Bogomolov, Sergiy and Donzé, Alexandre and Frehse, Goran and Grosu, Radu and Johnson, Taylor and Ladan, Hamed and Podelski, Andreas and Wehrle, Martin}, journal = {International Journal on Software Tools for Technology Transfer}, number = {4}, pages = {449 -- 467}, publisher = {Springer}, title = {{Guided search for hybrid systems based on coarse-grained space abstractions}}, doi = {10.1007/s10009-015-0393-y}, volume = {18}, year = {2016}, } @inproceedings{479, abstract = {Clinical guidelines and decision support systems (DSS) play an important role in daily practices of medicine. Many text-based guidelines have been encoded for work-flow simulation of DSS to automate health care. During the collaboration with Carle hospital to develop a DSS, we identify that, for some complex and life-critical diseases, it is highly desirable to automatically rigorously verify some complex temporal properties in guidelines, which brings new challenges to current simulation based DSS with limited support of automatical formal verification and real-time data analysis. In this paper, we conduct the first study on applying runtime verification to cooperate with current DSS based on real-time data. Within the proposed technique, a user-friendly domain specific language, named DRTV, is designed to specify vital real-time data sampled by medical devices and temporal properties originated from clinical guidelines. Some interfaces are developed for data acquisition and communication. Then, for medical practice scenarios described in DRTV model, we will automatically generate event sequences and runtime property verifier automata. If a temporal property violates, real-time warnings will be produced by the formal verifier and passed to medical DSS. We have used DRTV to specify different kinds of medical care scenarios, and applied the proposed technique to assist existing DSS. As presented in experiment results, in terms of warning detection, it outperforms the only use of DSS or human inspection, and improves the quality of clinical health care of hospital}, author = {Jiang, Yu and Liu, Han and Kong, Hui and Wang, Rui and Hosseini, Mohamad and Sun, Jiaguang and Sha, Lui}, booktitle = {Proceedings of the 38th International Conference on Software Engineering Companion }, location = {Austin, TX, USA}, pages = {112 -- 121}, publisher = {IEEE}, title = {{Use runtime verification to improve the quality of medical care practice}}, doi = {10.1145/2889160.2889233}, year = {2016}, } @inproceedings{1166, abstract = {POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.}, author = {Chatterjee, Krishnendu and Chmelik, Martin and Davies, Jessica}, booktitle = {Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence}, location = {Phoenix, AZ, USA}, pages = {3225 -- 3232}, publisher = {AAAI Press}, title = {{A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps}}, volume = {2016}, year = {2016}, } @inproceedings{1341, abstract = {In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.}, author = {Avni, Guy and Henzinger, Thomas A and Kupferman, Orna}, location = {Liverpool, United Kingdom}, pages = {153 -- 166}, publisher = {Springer}, title = {{Dynamic resource allocation games}}, doi = {10.1007/978-3-662-53354-3_13}, volume = {9928}, year = {2016}, } @phdthesis{1130, abstract = {In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion statements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver benchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency.}, author = {Tarrach, Thorsten}, issn = {2663-337X}, pages = {151}, publisher = {Institute of Science and Technology Austria}, title = {{Automatic synthesis of synchronisation primitives for concurrent programs}}, doi = {10.15479/at:ista:1130}, year = {2016}, } @inproceedings{1093, abstract = {We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. }, author = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana}, location = {Quebec City; Canada}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Linear distances between Markov chains}}, doi = {10.4230/LIPIcs.CONCUR.2016.20}, volume = {59}, year = {2016}, } @inproceedings{1234, abstract = {We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.}, author = {Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Petrov, Tatjana}, location = {Eindhoven, The Netherlands}, pages = {112 -- 129}, publisher = {Springer}, title = {{Faster statistical model checking for unbounded temporal properties}}, doi = {10.1007/978-3-662-49674-9_7}, volume = {9636}, year = {2016}, } @inproceedings{1230, abstract = {Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolictesting tool Crest and the model checker CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to Crest from 48% to 63% in the best case, and from 66% to 71% on average.}, author = {Daca, Przemyslaw and Gupta, Ashutosh and Henzinger, Thomas A}, location = {St. Petersburg, FL, USA}, pages = {328 -- 347}, publisher = {Springer}, title = {{Abstraction-driven concolic testing}}, doi = {10.1007/978-3-662-49122-5_16}, volume = {9583}, year = {2016}, } @inproceedings{1391, abstract = {We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as "the first array cell contains the array length," and "the array contains equally many minimal and maximal elements." These properties cannot be expressed in quantified fragments of the theory of arrays, nor in the theory of concatenation. Using reduction to counter machines, we show that the satisfiability problem of AFL is PSPACE-complete, and with a natural restriction the complexity decreases to NP. We also show that adding either universal quantifiers or concatenation leads to undecidability. AFL contains terms that fold a function over an array. We demonstrate that folding, a well-known concept from functional languages, allows us to concisely summarize loops that count over arrays, which occurs frequently in real-life programs. We provide a tool that can discharge proof obligations in AFL, and we demonstrate on practical examples that our decision procedure can solve a broad range of problems in symbolic testing and program verification.}, author = {Daca, Przemyslaw and Henzinger, Thomas A and Kupriyanov, Andrey}, location = {Toronto, Canada}, pages = {230 -- 248}, publisher = {Springer}, title = {{Array folds logic}}, doi = {10.1007/978-3-319-41540-6_13}, volume = {9780}, year = {2016}, } @inproceedings{1205, abstract = {In this paper, we present a formal model-driven engineering approach to establishing a safety-assured implementation of Multifunction vehicle bus controller (MVBC) based on the generic reference models and requirements described in the International Electrotechnical Commission (IEC) standard IEC-61375. First, the generic models described in IEC-61375 are translated into a network of timed automata, and some safety requirements tested in IEC-61375 are formalized as timed computation tree logic (TCTL) formulas. With the help of Uppaal, we check and debug whether the timed automata satisfy the formulas or not. Within this step, several logic inconsistencies in the original standard are detected and corrected. Then, we apply the tool Times to generate C code from the verified model, which was later synthesized into a real MVBC chip. Finally, the runtime verification tool RMOR is applied to verify some safety requirements at the implementation level. We set up a real platform with worldwide mostly used MVBC D113, and verify the correctness and the scalability of the synthesized MVBC chip more comprehensively. The errors in the standard has been confirmed and the resulted MVBC has been deployed in real train communication network.}, author = {Jiang, Yu and Liu, Han and Song, Houbing and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui}, location = {Limassol, Cyprus}, pages = {757 -- 763}, publisher = {Springer}, title = {{Safety assured formal model driven design of the multifunction vehicle bus controller}}, doi = {10.1007/978-3-319-48989-6_47}, volume = {9995}, year = {2016}, } @article{10794, abstract = {Mathematical models are of fundamental importance in the understanding of complex population dynamics. For instance, they can be used to predict the population evolution starting from different initial conditions or to test how a system responds to external perturbations. For this analysis to be meaningful in real applications, however, it is of paramount importance to choose an appropriate model structure and to infer the model parameters from measured data. While many parameter inference methods are available for models based on deterministic ordinary differential equations, the same does not hold for more detailed individual-based models. Here we consider, in particular, stochastic models in which the time evolution of the species abundances is described by a continuous-time Markov chain. These models are governed by a master equation that is typically difficult to solve. Consequently, traditional inference methods that rely on iterative evaluation of parameter likelihoods are computationally intractable. The aim of this paper is to present recent advances in parameter inference for continuous-time Markov chain models, based on a moment closure approximation of the parameter likelihood, and to investigate how these results can help in understanding, and ultimately controlling, complex systems in ecology. Specifically, we illustrate through an agricultural pest case study how parameters of a stochastic individual-based model can be identified from measured data and how the resulting model can be used to solve an optimal control problem in a stochastic setting. In particular, we show how the matter of determining the optimal combination of two different pest control methods can be formulated as a chance constrained optimization problem where the control action is modeled as a state reset, leading to a hybrid system formulation.}, author = {Parise, Francesca and Lygeros, John and Ruess, Jakob}, issn = {2296-665X}, journal = {Frontiers in Environmental Science}, keywords = {General Environmental Science}, publisher = {Frontiers}, title = {{Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study}}, doi = {10.3389/fenvs.2015.00042}, volume = {3}, year = {2015}, } @inproceedings{1498, abstract = {Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea.}, author = {Dragoi, Cezara and Henzinger, Thomas A and Zufferey, Damien}, isbn = {978-3-939897-80-4 }, location = {Asilomar, CA, United States}, pages = {90 -- 102}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{The need for language support for fault-tolerant distributed systems}}, doi = {10.4230/LIPIcs.SNAPL.2015.90}, volume = {32}, year = {2015}, } @inproceedings{1499, abstract = {We consider weighted automata with both positive and negative integer weights on edges and study the problem of synchronization using adaptive strategies that may only observe whether the current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.}, author = {Kretinsky, Jan and Larsen, Kim and Laursen, Simon and Srba, Jiří}, location = {Madrid, Spain}, pages = {142 -- 154}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Polynomial time decidability of weighted synchronization under partial observability}}, doi = {10.4230/LIPIcs.CONCUR.2015.142}, volume = {42}, year = {2015}, } @article{1539, abstract = {Many stochastic models of biochemical reaction networks contain some chemical species for which the number of molecules that are present in the system can only be finite (for instance due to conservation laws), but also other species that can be present in arbitrarily large amounts. The prime example of such networks are models of gene expression, which typically contain a small and finite number of possible states for the promoter but an infinite number of possible states for the amount of mRNA and protein. One of the main approaches to analyze such models is through the use of equations for the time evolution of moments of the chemical species. Recently, a new approach based on conditional moments of the species with infinite state space given all the different possible states of the finite species has been proposed. It was argued that this approach allows one to capture more details about the full underlying probability distribution with a smaller number of equations. Here, I show that the result that less moments provide more information can only stem from an unnecessarily complicated description of the system in the classical formulation. The foundation of this argument will be the derivation of moment equations that describe the complete probability distribution over the finite state space but only low-order moments over the infinite state space. I will show that the number of equations that is needed is always less than what was previously claimed and always less than the number of conditional moment equations up to the same order. To support these arguments, a symbolic algorithm is provided that can be used to derive minimal systems of unconditional moment equations for models with partially finite state space. }, author = {Ruess, Jakob}, journal = {Journal of Chemical Physics}, number = {24}, publisher = {American Institute of Physics}, title = {{Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space}}, doi = {10.1063/1.4937937}, volume = {143}, year = {2015}, } @article{1538, abstract = {Systems biology rests on the idea that biological complexity can be better unraveled through the interplay of modeling and experimentation. However, the success of this approach depends critically on the informativeness of the chosen experiments, which is usually unknown a priori. Here, we propose a systematic scheme based on iterations of optimal experiment design, flow cytometry experiments, and Bayesian parameter inference to guide the discovery process in the case of stochastic biochemical reaction networks. To illustrate the benefit of our methodology, we apply it to the characterization of an engineered light-inducible gene expression circuit in yeast and compare the performance of the resulting model with models identified from nonoptimal experiments. In particular, we compare the parameter posterior distributions and the precision to which the outcome of future experiments can be predicted. Moreover, we illustrate how the identified stochastic model can be used to determine light induction patterns that make either the average amount of protein or the variability in a population of cells follow a desired profile. Our results show that optimal experiment design allows one to derive models that are accurate enough to precisely predict and regulate the protein expression in heterogeneous cell populations over extended periods of time.}, author = {Ruess, Jakob and Parise, Francesca and Milias Argeitis, Andreas and Khammash, Mustafa and Lygeros, John}, journal = {PNAS}, number = {26}, pages = {8148 -- 8153}, publisher = {National Academy of Sciences}, title = {{Iterative experiment design guides the characterization of a light-inducible gene expression circuit}}, doi = {10.1073/pnas.1423947112}, volume = {112}, year = {2015}, } @inproceedings{1541, abstract = {We present XSpeed a parallel state-space exploration algorithm for continuous systems with linear dynamics and nondeterministic inputs. The motivation of having parallel algorithms is to exploit the computational power of multi-core processors to speed-up performance. The parallelization is achieved on two fronts. First, we propose a parallel implementation of the support function algorithm by sampling functions in parallel. Second, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input. A GP-GPU implementation is also presented following a lazy evaluation strategy on support functions. The parallel algorithms are implemented in the tool XSpeed. We evaluated the performance on two benchmarks including an 28 dimension Helicopter model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experiments illustrate that our parallel algorithm with time slicing not only speeds-up performance but also improves precision.}, author = {Ray, Rajarshi and Gurung, Amit and Das, Binayak and Bartocci, Ezio and Bogomolov, Sergiy and Grosu, Radu}, location = {Haifa, Israel}, pages = {3 -- 18}, publisher = {Springer}, title = {{XSpeed: Accelerating reachability analysis on multi-core processors}}, doi = {10.1007/978-3-319-26287-1_1}, volume = {9434}, year = {2015}, } @inproceedings{1594, abstract = {Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.}, author = {Forejt, Vojtěch and Krčál, Jan and Kretinsky, Jan}, location = {Suva, Fiji}, pages = {162 -- 177}, publisher = {Springer}, title = {{Controller synthesis for MDPs and frequency LTL\GU}}, doi = {10.1007/978-3-662-48899-7_12}, volume = {9450}, year = {2015}, } @inproceedings{1601, abstract = {We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.}, author = {Babiak, Tomáš and Blahoudek, František and Duret Lutz, Alexandre and Klein, Joachim and Kretinsky, Jan and Mueller, Daniel and Parker, David and Strejček, Jan}, location = {San Francisco, CA, United States}, pages = {479 -- 486}, publisher = {Springer}, title = {{The Hanoi omega-automata format}}, doi = {10.1007/978-3-319-21690-4_31}, volume = {9206}, year = {2015}, } @inproceedings{1605, abstract = {Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.}, author = {Bogomolov, Sergiy and Schilling, Christian and Bartocci, Ezio and Batt, Grégory and Kong, Hui and Grosu, Radu}, location = {Haifa, Israel}, pages = {19 -- 35}, publisher = {Springer}, title = {{Abstraction-based parameter synthesis for multiaffine systems}}, doi = {10.1007/978-3-319-26287-1_2}, volume = {9434}, year = {2015}, } @inproceedings{1606, abstract = {In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.}, author = {Nguyen, Luan and Schilling, Christian and Bogomolov, Sergiy and Johnson, Taylor}, booktitle = {6th International Conference}, isbn = {978-3-319-23819-7}, location = {Vienna, Austria}, pages = {281 -- 286}, publisher = {Springer Nature}, title = {{Runtime verification for hybrid analysis tools}}, doi = {10.1007/978-3-319-23820-3_19}, volume = {9333}, year = {2015}, } @inproceedings{1658, abstract = {Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space.}, author = {Bogomolov, Sergiy and Henzinger, Thomas A and Podelski, Andreas and Ruess, Jakob and Schilling, Christian}, location = {Nantes, France}, pages = {77 -- 89}, publisher = {Springer}, title = {{Adaptive moment closure for parameter inference of biochemical reaction networks}}, doi = {10.1007/978-3-319-23401-4_8}, volume = {9308}, year = {2015}, } @inproceedings{1670, abstract = {Planning in hybrid domains poses a special challenge due to the involved mixed discrete-continuous dynamics. A recent solving approach for such domains is based on applying model checking techniques on a translation of PDDL+ planning problems to hybrid automata. However, the proposed translation is limited because must behavior is only overapproximated, and hence, processes and events are not reflected exactly. In this paper, we present the theoretical foundation of an exact PDDL+ translation. We propose a schema to convert a hybrid automaton with must transitions into an equivalent hybrid automaton featuring only may transitions.}, author = {Bogomolov, Sergiy and Magazzeni, Daniele and Minopoli, Stefano and Wehrle, Martin}, location = {Jerusalem, Israel}, pages = {42 -- 46}, publisher = {AAAI Press}, title = {{PDDL+ planning with hybrid automata: Foundations of translating must behavior}}, year = {2015}, } @article{1680, abstract = {We consider the satisfiability problem for modal logic over first-order definable classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008] that modal logic is decidable over classes definable by universal Horn formulae. We provide a full classification of Horn formulae with respect to the complexity of the corresponding satisfiability problem. It turns out, that except for the trivial case of inconsistent formulae, local satisfiability is eitherNP-complete or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete, or ExpTime-complete. We also show that the finite satisfiability problem for modal logic over Horn definable classes of frames is decidable. On the negative side, we show undecidability of two related problems. First, we exhibit a simple universal three-variable formula defining the class of frames over which modal logic is undecidable. Second, we consider the satisfiability problem of bimodal logic over Horn definable classes of frames, and also present a formula leading to undecidability.}, author = {Michaliszyn, Jakub and Otop, Jan and Kieroňski, Emanuel}, journal = {ACM Transactions on Computational Logic}, number = {1}, publisher = {ACM}, title = {{On the decidability of elementary modal logics}}, doi = {10.1145/2817825}, volume = {17}, year = {2015}, } @inproceedings{1692, abstract = {Computing an approximation of the reachable states of a hybrid system is a challenge, mainly because overapproximating the solutions of ODEs with a finite number of sets does not scale well. Using template polyhedra can greatly reduce the computational complexity, since it replaces complex operations on sets with a small number of optimization problems. However, the use of templates may make the over-approximation too conservative. Spurious transitions, which are falsely considered reachable, are particularly detrimental to performance and accuracy, and may exacerbate the state explosion problem. In this paper, we examine how spurious transitions can be avoided with minimal computational effort. To this end, detecting spurious transitions is reduced to the well-known problem of showing that two convex sets are disjoint by finding a hyperplane that separates them. We generalize this to owpipes by considering hyperplanes that evolve with time in correspondence to the dynamics of the system. The approach is implemented in the model checker SpaceEx and demonstrated on examples.}, author = {Frehse, Goran and Bogomolov, Sergiy and Greitschus, Marius and Strump, Thomas and Podelski, Andreas}, booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control}, isbn = {978-1-4503-3433-4}, location = {Seattle, WA, United States}, pages = {149 -- 158}, publisher = {ACM}, title = {{Eliminating spurious transitions in reachability with support functions}}, doi = {10.1145/2728606.2728622}, year = {2015}, } @inproceedings{1690, abstract = {A number of powerful and scalable hybrid systems model checkers have recently emerged. Although all of them honor roughly the same hybrid systems semantics, they have drastically different model description languages. This situation (a) makes it difficult to quickly evaluate a specific hybrid automaton model using the different tools, (b) obstructs comparisons of reachability approaches, and (c) impedes the widespread application of research results that perform model modification and could benefit many of the tools. In this paper, we present Hyst, a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of HyCreate, Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation passes that serve to both ease the translation and potentially improve reachability results for the supported tools. Although these model transformation passes could be implemented within each tool, the Hyst approach provides a single place for model modification, generating modified input sources for the unmodified target tools. Our evaluation demonstrates Hyst is capable of automatically translating benchmarks in several classes (including affine and nonlinear hybrid automata) to the input formats of several tools. Additionally, we illustrate a general model transformation pass based on pseudo-invariants implemented in Hyst that illustrates the reachability improvement.}, author = {Bak, Stanley and Bogomolov, Sergiy and Johnson, Taylor}, location = {Seattle, WA, United States}, pages = {128 -- 133}, publisher = {Springer}, title = {{HYST: A source transformation and translation tool for hybrid automaton models}}, doi = {10.1145/2728606.2728630}, year = {2015}, } @article{1698, abstract = {In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf objectives are coNP-complete.}, author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A and Rabinovich, Alexander and Raskin, Jean}, journal = {Information and Computation}, number = {4}, pages = {177 -- 196}, publisher = {Elsevier}, title = {{The complexity of multi-mean-payoff and multi-energy games}}, doi = {10.1016/j.ic.2015.03.001}, volume = {241}, year = {2015}, } @article{1808, author = {Gupta, Ashutosh and Henzinger, Thomas A}, journal = {ACM Transactions on Modeling and Computer Simulation}, number = {2}, publisher = {ACM}, title = {{Guest editors' introduction to special issue on computational methods in systems biology}}, doi = {10.1145/2745799}, volume = {25}, year = {2015}, } @inproceedings{1836, abstract = {In the standard framework for worst-case execution time (WCET) analysis of programs, the main data structure is a single instance of integer linear programming (ILP) that represents the whole program. The instance of this NP-hard problem must be solved to find an estimate forWCET, and it must be refined if the estimate is not tight.We propose a new framework for WCET analysis, based on abstract segment trees (ASTs) as the main data structure. The ASTs have two advantages. First, they allow computing WCET by solving a number of independent small ILP instances. Second, ASTs store more expressive constraints, thus enabling a more efficient and precise refinement procedure. In order to realize our framework algorithmically, we develop an algorithm for WCET estimation on ASTs, and we develop an interpolation-based counterexample-guided refinement scheme for ASTs. Furthermore, we extend our framework to obtain parametric estimates of WCET. We experimentally evaluate our approach on a set of examples from WCET benchmark suites and linear-algebra packages. We show that our analysis, with comparable effort, provides WCET estimates that in many cases significantly improve those computed by existing tools.}, author = {Cerny, Pavol and Henzinger, Thomas A and Kovács, Laura and Radhakrishna, Arjun and Zwirchmayr, Jakob}, location = {London, United Kingdom}, pages = {105 -- 131}, publisher = {Springer}, title = {{Segment abstraction for worst-case execution time analysis}}, doi = {10.1007/978-3-662-46669-8_5}, volume = {9032}, year = {2015}, } @article{1846, abstract = {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 known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.}, author = {Beneš, Nikola and Kretinsky, Jan and Larsen, Kim and Möller, Mikael and Sickert, Salomon and Srba, Jiří}, journal = {Acta Informatica}, number = {2-3}, pages = {269 -- 297}, publisher = {Springer}, title = {{Refinement checking on parametric modal transition systems}}, doi = {10.1007/s00236-015-0215-4}, volume = {52}, year = {2015}, } @article{1840, abstract = {In this paper, we present a method for reducing a regular, discrete-time Markov chain (DTMC) to another DTMC with a given, typically much smaller number of states. The cost of reduction is defined as the Kullback-Leibler divergence rate between a projection of the original process through a partition function and a DTMC on the correspondingly partitioned state space. Finding the reduced model with minimal cost is computationally expensive, as it requires an exhaustive search among all state space partitions, and an exact evaluation of the reduction cost for each candidate partition. Our approach deals with the latter problem by minimizing an upper bound on the reduction cost instead of minimizing the exact cost. The proposed upper bound is easy to compute and it is tight if the original chain is lumpable with respect to the partition. Then, we express the problem in the form of information bottleneck optimization, and propose using the agglomerative information bottleneck algorithm for searching a suboptimal partition greedily, rather than exhaustively. The theory is illustrated with examples and one application scenario in the context of modeling bio-molecular interactions.}, author = {Geiger, Bernhard and Petrov, Tatjana and Kubin, Gernot and Koeppl, Heinz}, issn = {0018-9286}, journal = {IEEE Transactions on Automatic Control}, number = {4}, pages = {1010 -- 1022}, publisher = {IEEE}, title = {{Optimal Kullback-Leibler aggregation via information bottleneck}}, doi = {10.1109/TAC.2014.2364971}, volume = {60}, year = {2015}, } @article{1861, abstract = {Continuous-time Markov chains are commonly used in practice for modeling biochemical reaction networks in which the inherent randomness of themolecular interactions cannot be ignored. This has motivated recent research effort into methods for parameter inference and experiment design for such models. The major difficulty is that such methods usually require one to iteratively solve the chemical master equation that governs the time evolution of the probability distribution of the system. This, however, is rarely possible, and even approximation techniques remain limited to relatively small and simple systems. An alternative explored in this article is to base methods on only some low-order moments of the entire probability distribution. We summarize the theory behind such moment-based methods for parameter inference and experiment design and provide new case studies where we investigate their performance.}, author = {Ruess, Jakob and Lygeros, John}, journal = {ACM Transactions on Modeling and Computer Simulation}, number = {2}, publisher = {ACM}, title = {{Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks}}, doi = {10.1145/2688906}, volume = {25}, year = {2015}, } @article{1866, author = {Henzinger, Thomas A and Raskin, Jean}, journal = {Communications of the ACM}, number = {2}, pages = {86--86}, publisher = {ACM}, title = {{The equivalence problem for finite automata: Technical perspective}}, doi = {10.1145/2701001}, volume = {58}, year = {2015}, } @inproceedings{1882, abstract = {We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.}, author = {Fahrenberg, Uli and Kretinsky, Jan and Legay, Axel and Traonouez, Louis}, location = {Bertinoro, Italy}, pages = {306 -- 324}, publisher = {Springer}, title = {{Compositionality for quantitative specifications}}, doi = {10.1007/978-3-319-15317-9_19}, volume = {8997}, year = {2015}, } @inproceedings{1992, abstract = {We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings. We claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising. In the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula.}, author = {Gupta, Ashutosh and Henzinger, Thomas A and Radhakrishna, Arjun and Samanta, Roopsha and Tarrach, Thorsten}, isbn = {978-1-4503-3300-9}, location = {Mumbai, India}, pages = {433 -- 444}, publisher = {ACM}, title = {{Succinct representation of concurrent trace sets}}, doi = {10.1145/2676726.2677008}, year = {2015}, } @article{1832, abstract = {Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. }, author = {Chakraborty, Soham and Henzinger, Thomas A and Sezgin, Ali and Vafeiadis, Viktor}, journal = {Logical Methods in Computer Science}, number = {1}, publisher = {International Federation of Computational Logic}, title = {{Aspect-oriented linearizability proofs}}, doi = {10.2168/LMCS-11(1:20)2015}, volume = {11}, year = {2015}, } @article{1731, abstract = {We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (both players interact simultaneously); and (b) turn-based (both players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. In this work we present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games. }, author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Henzinger, Thomas A}, journal = {Information and Computation}, number = {12}, pages = {3 -- 16}, publisher = {Elsevier}, title = {{Randomness for free}}, doi = {10.1016/j.ic.2015.06.003}, volume = {245}, year = {2015}, } @article{1856, abstract = {The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε > 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara and Singh, Rohit}, journal = {Journal of the ACM}, number = {1}, publisher = {ACM}, title = {{Measuring and synthesizing systems in probabilistic environments}}, doi = {10.1145/2699430}, volume = {62}, year = {2015}, } @inproceedings{1657, abstract = {We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. }, author = {Chatterjee, Krishnendu and Komárková, Zuzana and Kretinsky, Jan}, location = {Kyoto, Japan}, pages = {244 -- 256}, publisher = {IEEE}, title = {{Unifying two views on multiple mean-payoff objectives in Markov decision processes}}, doi = {10.1109/LICS.2015.32}, year = {2015}, } @inproceedings{1656, abstract = {Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan}, booktitle = {Proceedings - Symposium on Logic in Computer Science}, location = {Kyoto, Japan}, publisher = {IEEE}, title = {{Nested weighted automata}}, doi = {10.1109/LICS.2015.72}, volume = {2015-July}, year = {2015}, } @misc{5436, abstract = {Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan}, issn = {2664-1690}, pages = {29}, publisher = {IST Austria}, title = {{Nested weighted automata}}, doi = {10.15479/AT:IST-2015-170-v2-2}, year = {2015}, } @inproceedings{1659, abstract = {The target discounted-sum problem is the following: Given a rational discount factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata.}, author = {Boker, Udi and Henzinger, Thomas A and Otop, Jan}, booktitle = {LICS}, issn = {1043-6871 }, location = {Kyoto, Japan}, pages = {750 -- 761}, publisher = {IEEE}, title = {{The target discounted-sum problem}}, doi = {10.1109/LICS.2015.74}, year = {2015}, } @inproceedings{1610, abstract = {The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Ibsen-Jensen, Rasmus and Otop, Jan}, booktitle = {42nd International Colloquium}, isbn = {978-3-662-47665-9}, location = {Kyoto, Japan}, number = {Part II}, pages = {121 -- 133}, publisher = {Springer Nature}, title = {{Edit distance for pushdown automata}}, doi = {10.1007/978-3-662-47666-6_10}, volume = {9135}, year = {2015}, } @misc{5439, abstract = {The target discounted-sum problem is the following: Given a rational discount factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata. }, author = {Boker, Udi and Henzinger, Thomas A and Otop, Jan}, issn = {2664-1690}, pages = {20}, publisher = {IST Austria}, title = {{The target discounted-sum problem}}, doi = {10.15479/AT:IST-2015-335-v1-1}, year = {2015}, } @inproceedings{1502, abstract = {We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system.}, author = {Beneš, Nikola and Daca, Przemyslaw and Henzinger, Thomas A and Kretinsky, Jan and Nickovic, Dejan}, isbn = {978-1-4503-3471-6}, location = {Montreal, QC, Canada}, pages = {101 -- 110}, publisher = {ACM}, title = {{Complete composition operators for IOCO-testing theory}}, doi = {10.1145/2737166.2737175}, year = {2015}, } @article{1501, abstract = {We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. }, author = {Chatterjee, Krishnendu and Chmelik, Martin and Daca, Przemyslaw}, journal = {Formal Methods in System Design}, number = {2}, pages = {230 -- 264}, publisher = {Springer}, title = {{CEGAR for compositional analysis of qualitative properties in Markov decision processes}}, doi = {10.1007/s10703-015-0235-2}, volume = {47}, year = {2015}, }