@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},
}
@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},
}
@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},
pages = {151},
publisher = {IST Austria},
title = {{Automatic synthesis of synchronisation primitives for concurrent programs}},
year = {2016},
}
@inproceedings{1256,
abstract = {Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform.},
author = {Jiang, Yu and Yang, Yixiao and Liu, Han and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui},
location = {Vienna, Austria},
publisher = {IEEE},
title = {{From stateflow simulation to verified implementation: A verification approach and a real-time train controller design}},
doi = {10.1109/RTAS.2016.7461337},
year = {2016},
}
@inproceedings{1390,
abstract = {The goal of automatic program repair is to identify a set of syntactic changes that can turn a program that is incorrect with respect
to a given specification into a correct one. Existing program repair techniques typically aim to find any program that meets the given specification. Such “best-effort” strategies can end up generating a program that is quite different from the original one. Novel techniques have been proposed to compute syntactically minimal program fixes, but the smallest syntactic fix to a program can still significantly alter the original program’s behaviour. We propose a new approach to program repair based on program distances, which can quantify changes not only to the program syntax but also to the program semantics. We call this the quantitative program repair problem where the “optimal” repair is derived using multiple distances. We implement a solution to the quantitative repair
problem in a prototype tool called Qlose
(Quantitatively close), using the program synthesizer Sketch. We evaluate the effectiveness of different distances in obtaining desirable repairs by evaluating
Qlose on programs taken from educational tools such as CodeHunt and edX.},
author = {D'Antoni, Loris and Samanta, Roopsha and Singh, Rishabh},
location = {Toronto, Canada},
pages = {383 -- 401},
publisher = {Springer},
title = {{QLOSE: Program repair with quantitative objectives}},
doi = {10.1007/978-3-319-41540-6_21},
volume = {9780},
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},
}
@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},
}
@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{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{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{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{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},
}
@inproceedings{1138,
abstract = {Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium},
location = {New York, NY, USA},
pages = {76 -- 85},
publisher = {IEEE},
title = {{Quantitative automata under probabilistic semantics}},
doi = {10.1145/2933575.2933588},
year = {2016},
}
@inproceedings{1227,
abstract = {Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples.},
author = {Kong, Hui and Bartocci, Ezio and Bogomolov, Sergiy and Grosu, Radu and Henzinger, Thomas A and Jiang, Yu and Schilling, Christian},
location = {Grenoble, France},
pages = {128 -- 144},
publisher = {Springer},
title = {{Discrete abstraction of multiaffine systems}},
doi = {10.1007/978-3-319-47151-8_9},
volume = {9957},
year = {2016},
}
@inproceedings{1335,
abstract = {In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted ω-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted ω-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted ω-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
location = {Edinburgh, United Kingdom},
pages = {23 -- 38},
publisher = {Springer},
title = {{Quantitative monitor automata}},
doi = {10.1007/978-3-662-53413-7_2},
volume = {9837},
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{1134,
abstract = {Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.},
author = {Duggirala, Parasara and Fan, Chuchu and Potok, Matthew and Qi, Bolun and Mitra, Sayan and Viswanathan, Mahesh and Bak, Stanley and Bogomolov, Sergiy and Johnson, Taylor and Nguyen, Luan and Schilling, Christian and Sogokon, Andrew and Tran, Hoang and Xiang, Weiming},
booktitle = {2016 IEEE Conference on Control Applications},
location = {Buenos Aires, Argentina },
publisher = {IEEE},
title = {{Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP}},
doi = {10.1109/CCA.2016.7587948},
year = {2016},
}
@inproceedings{1090,
abstract = { While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
location = {Krakow; Poland},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Nested weighted limit-average automata of bounded width}},
doi = {10.4230/LIPIcs.MFCS.2016.24},
volume = {58},
year = {2016},
}
@inproceedings{1095,
abstract = { The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. },
author = {Haas, Andreas and Henzinger, Thomas A and Holzer, Andreas and Kirsch, Christoph and Lippautz, Michael and Payer, Hannes and Sezgin, Ali and Sokolova, Ana and Veith, Helmut},
booktitle = {Leibniz International Proceedings in Informatics},
location = {Quebec City; Canada},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Local linearizability for concurrent container-type data structures}},
doi = {10.4230/LIPIcs.CONCUR.2016.6},
volume = {59},
year = {2016},
}
@inproceedings{1103,
abstract = {We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA.},
author = {Gurung, Amit and Deka, Arup and Bartocci, Ezio and Bogomolov, Sergiy and Grosu, Radu and Ray, Rajarshi},
location = {Kanpur, India },
publisher = {IEEE},
title = {{Parallel reachability analysis for hybrid systems}},
doi = {10.1109/MEMCOD.2016.7797741},
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{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},
}
@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},
}
@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},
}
@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},
}
@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{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},
}
@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{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{1729,
abstract = {We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of such sequences produced under a non-preemptive scheduler. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and rules for inserting synchronization. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient, and, since it does not require explicit specifications, is more practical than the conventional approach based on user-provided assertions.},
author = {Cerny, Pavol and Clarke, Edmund and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Samanta, Roopsha and Tarrach, Thorsten},
location = {San Francisco, CA, United States},
pages = {180 -- 197},
publisher = {Springer},
title = {{From non-preemptive to preemptive scheduling using synchronization synthesis}},
doi = {10.1007/978-3-319-21668-3_11},
volume = {9207},
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{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{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},
}
@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},
}
@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},
}
@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},
}
@misc{5549,
abstract = {This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.
We extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.
The archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.
To execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.
The archive contains scripts that (if run often enough) reproduces the data presented in the publication.},
author = {Fellner, Andreas},
keyword = {Markov Decision Process, Decision Tree, Probabilistic Verification, Counterexample Explanation},
publisher = {IST Austria},
title = {{Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes}},
doi = {10.15479/AT:ISTA:28},
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{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},
}
@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{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},
location = {Vienna, Austria},
pages = {281 -- 286},
publisher = {Springer},
title = {{Runtime verification for hybrid analysis tools}},
doi = {10.1007/978-3-319-23820-3_19},
volume = {9333},
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{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},
}
@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},
}
@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{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},
}
@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},
}
@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{1835,
abstract = {The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs –an important problem of interest in evolutionary biology– more efficiently than the classical simulation method. We specify the property in linear temporal logics. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.},
author = {Giacobbe, Mirco and Guet, Calin C and Gupta, Ashutosh and Henzinger, Thomas A and Paixao, Tiago and Petrov, Tatjana},
location = {London, United Kingdom},
pages = {469 -- 483},
publisher = {Springer},
title = {{Model checking gene regulatory networks}},
doi = {10.1007/978-3-662-46681-0_47},
volume = {9035},
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},
}
@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},
}
@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{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},
}
@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},
}
@inproceedings{1689,
abstract = {We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study.},
author = {Svoreňová, Mária and Kretinsky, Jan and Chmelik, Martin and Chatterjee, Krishnendu and Cěrná, Ivana and Belta, Cǎlin},
booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control},
location = {Seattle, WA, United States},
pages = {259 -- 268},
publisher = {ACM},
title = {{Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games}},
doi = {10.1145/2728606.2728608},
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{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{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},
}
@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},
location = {Kyoto, Japan},
number = {Part II},
pages = {121 -- 133},
publisher = {Springer},
title = {{Edit distance for pushdown automata}},
doi = {10.1007/978-3-662-47666-6_10},
volume = {9135},
year = {2015},
}
@inproceedings{1603,
abstract = {For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.
The key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour.},
author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Chmelik, Martin and Fellner, Andreas and Kretinsky, Jan},
location = {San Francisco, CA, United States},
pages = {158 -- 177},
publisher = {Springer},
title = {{Counterexample explanation by learning small strategies in Markov decision processes}},
doi = {10.1007/978-3-319-21690-4_10},
volume = {9206},
year = {2015},
}
@inproceedings{1870,
abstract = {We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer 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. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using setsimilarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers.},
author = {Henzinger, Thomas A and Otop, Jan and Samanta, Roopsha},
booktitle = {Leibniz International Proceedings in Informatics, LIPIcs},
location = {Delhi, India},
pages = {431 -- 443},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Lipschitz robustness of finite-state transducers}},
doi = {10.4230/LIPIcs.FSTTCS.2014.431},
volume = {29},
year = {2014},
}
@inproceedings{1875,
abstract = {We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.},
author = {Samanta, Roopsha and Olivo, Oswaldo and Allen, Emerson},
editor = {Müller-Olm, Markus and Seidl, Helmut},
location = {Munich, Germany},
pages = {268 -- 284},
publisher = {Springer},
title = {{Cost-aware automatic program repair}},
doi = {10.1007/978-3-319-10936-7_17},
volume = {8723},
year = {2014},
}
@article{2056,
abstract = {We consider a continuous-time Markov chain (CTMC) whose state space is partitioned into aggregates, and each aggregate is assigned a probability measure. A sufficient condition for defining a CTMC over the aggregates is presented as a variant of weak lumpability, which also characterizes that the measure over the original process can be recovered from that of the aggregated one. We show how the applicability of de-aggregation depends on the initial distribution. The application section is devoted to illustrate how the developed theory aids in reducing CTMC models of biochemical systems particularly in connection to protein-protein interactions. We assume that the model is written by a biologist in form of site-graph-rewrite rules. Site-graph-rewrite rules compactly express that, often, only a local context of a protein (instead of a full molecular species) needs to be in a certain configuration in order to trigger a reaction event. This observation leads to suitable aggregate Markov chains with smaller state spaces, thereby providing sufficient reduction in computational complexity. This is further exemplified in two case studies: simple unbounded polymerization and early EGFR/insulin crosstalk.},
author = {Ganguly, Arnab and Petrov, Tatjana and Koeppl, Heinz},
journal = {Journal of Mathematical Biology},
number = {3},
pages = {767 -- 797},
publisher = {Springer},
title = {{Markov chain aggregation and its applications to combinatorial reaction networks}},
doi = {10.1007/s00285-013-0738-7},
volume = {69},
year = {2014},
}
@misc{5428,
abstract = {Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms.
In this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan and Velner, Yaron},
issn = {2664-1690},
pages = {26},
publisher = {IST Austria},
title = {{Quantitative fair simulation games}},
doi = {10.15479/AT:IST-2014-315-v1-1},
year = {2014},
}
@inproceedings{2239,
abstract = {The analysis of the energy consumption of software is an important goal for quantitative formal methods. Current methods, using weighted transition systems or energy games, model the energy source as an ideal resource whose status is characterized by one number, namely the amount of remaining energy. Real batteries, however, exhibit behaviors that can deviate substantially from an ideal energy resource. Based on a discretization of a standard continuous battery model, we introduce battery transition systems. In this model, a battery is viewed as consisting of two parts-the available-charge tank and the bound-charge tank. Any charge or discharge is applied to the available-charge tank. Over time, the energy from each tank diffuses to the other tank. Battery transition systems are infinite state systems that, being not well-structured, fall into no decidable class that is known to us. Nonetheless, we are able to prove that the !-regular modelchecking problem is decidable for battery transition systems. We also present a case study on the verification of control programs for energy-constrained semi-autonomous robots.},
author = {Boker, Udi and Henzinger, Thomas A and Radhakrishna, Arjun},
isbn = {978-145032544-8},
location = {San Diego, USA},
number = {1},
pages = {595 -- 606},
publisher = {ACM},
title = {{Battery transition systems}},
doi = {10.1145/2535838.2535875},
volume = {49},
year = {2014},
}
@inproceedings{2190,
abstract = {We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.},
author = {Esparza, Javier and Kretinsky, Jan},
pages = {192 -- 208},
publisher = {Springer},
title = {{From LTL to deterministic automata: A safraless compositional approach}},
doi = {10.1007/978-3-319-08867-9_13},
volume = {8559},
year = {2014},
}
@inproceedings{2063,
abstract = {We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs 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 ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.},
author = {Chatterjee, Krishnendu and Chmelik, Martin and Daca, Przemyslaw},
location = {Vienna, Austria},
pages = {473 -- 490},
publisher = {Springer},
title = {{CEGAR for qualitative analysis of probabilistic systems}},
doi = {10.1007/978-3-319-08867-9_31},
volume = {8559},
year = {2014},
}
@misc{5411,
abstract = {Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing.
In this paper, we study compositional properties of the IOCO-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the IOCO conformance relation, the resulting methodology can be applied to a broader class of systems.},
author = {Daca, Przemyslaw and Henzinger, Thomas A and Krenn, Willibald and Nickovic, Dejan},
issn = {2664-1690},
pages = {20},
publisher = {IST Austria},
title = {{Compositional specifications for IOCO testing}},
doi = {10.15479/AT:IST-2014-148-v2-1},
year = {2014},
}
@misc{5416,
abstract = {As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.The contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem.},
author = {Henzinger, Thomas A and Otop, Jan},
issn = {2664-1690},
pages = {22},
publisher = {IST Austria},
title = {{Model measuring for hybrid systems}},
doi = {10.15479/AT:IST-2014-171-v1-1},
year = {2014},
}
@misc{5417,
abstract = {We define the model-measuring problem: given a model M and specification φ, what is the maximal distance ρ such that all models M'within distance ρ from M satisfy (or violate)φ. The model measuring problem presupposes a distance function on models. We concentrate on automatic distance functions, which are defined by weighted automata.
The model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification, and robustness problems that measure how much a model can be perturbed without violating the specification.
We show that for automatic distance functions, and ω-regular linear-time and branching-time specifications, the model-measuring problem can be solved.
We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for standard word and tree automata by the optimal-weight question for the weighted versions of these automata. We consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging.
We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications.},
author = {Henzinger, Thomas A and Otop, Jan},
issn = {2664-1690},
pages = {14},
publisher = {IST Austria},
title = {{From model checking to model measuring}},
doi = {10.15479/AT:IST-2014-172-v1-1},
year = {2014},
}
@inproceedings{1869,
abstract = {Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified firstorder formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes.},
author = {Hofferek, Georg and Gupta, Ashutosh},
booktitle = {HVC 2014},
editor = {Yahav, Eran},
location = {Haifa, Israel},
pages = {68 -- 74},
publisher = {Springer},
title = {{Suraq - a controller synthesis tool using uninterpreted functions}},
doi = {10.1007/978-3-319-13338-6_6},
volume = {8855},
year = {2014},
}
@inproceedings{2026,
abstract = {We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra’s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.},
author = {Komárková, Zuzana and Kretinsky, Jan},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
editor = {Cassez, Franck and Raskin, Jean-François},
location = {Sydney, Australia},
pages = {235 -- 241},
publisher = {Springer},
title = {{Rabinizer 3: Safraless translation of ltl to small deterministic automata}},
doi = {10.1007/978-3-319-11936-6_17},
volume = {8837},
year = {2014},
}
@article{2038,
abstract = {Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with "controlled accumulation," allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable.},
author = {Boker, Udi and Chatterjee, Krishnendu and Henzinger, Thomas A and Kupferman, Orna},
journal = {ACM Transactions on Computational Logic (TOCL)},
number = {4},
publisher = {ACM},
title = {{Temporal specifications with accumulative values}},
doi = {10.1145/2629686},
volume = {15},
year = {2014},
}
@inproceedings{1702,
abstract = {In this paper we present INTERHORN, a solver for recursion-free Horn clauses. The main application domain of INTERHORN lies in solving interpolation problems arising in software verification. We show how a range of interpolation problems, including path, transition, nested, state/transition and well-founded interpolation can be handled directly by INTERHORN. By detailing these interpolation problems and their Horn clause representations, we hope to encourage the emergence of a common back-end interpolation interface useful for diverse verification tools.},
author = {Gupta, Ashutosh and Popeea, Corneliu and Rybalchenko, Andrey},
booktitle = {Electronic Proceedings in Theoretical Computer Science, EPTCS},
location = {Vienna, Austria},
pages = {31 -- 38},
publisher = {Open Publishing},
title = {{Generalised interpolation by solving recursion free-horn clauses}},
doi = {10.4204/EPTCS.169.5},
volume = {169},
year = {2014},
}
@inproceedings{1872,
abstract = {Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover.},
author = {Gupta, Ashutosh and Kovács, Laura and Kragl, Bernhard and Voronkov, Andrei},
booktitle = {ATVA 2014},
editor = {Cassez, Franck and Raskin, Jean-François},
location = {Sydney, Australia},
pages = {185 -- 200},
publisher = {Springer},
title = {{Extensional crisis and proving identity}},
doi = {10.1007/978-3-319-11936-6_14},
volume = {8837},
year = {2014},
}
@inproceedings{2027,
abstract = {We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.},
author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Chmelik, Martin and Forejt, Vojtěch and Kretinsky, Jan and Kwiatkowska, Marta and Parker, David and Ujma, Mateusz},
booktitle = { Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
editor = {Cassez, Franck and Raskin, Jean-François},
location = {Sydney, Australia},
pages = {98 -- 114},
publisher = {Society of Industrial and Applied Mathematics},
title = {{Verification of markov decision processes using learning algorithms}},
doi = {10.1007/978-3-319-11936-6_8},
volume = {8837},
year = {2014},
}
@inproceedings{2053,
abstract = {In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems.},
author = {Hermanns, Holger and Krčál, Jan and Kretinsky, Jan},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
editor = {Baldan, Paolo and Gorla, Daniele},
location = {Rome, Italy},
pages = {249 -- 265},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Probabilistic bisimulation: Naturally on distributions}},
doi = {10.1007/978-3-662-44584-6_18},
volume = {8704},
year = {2014},
}
@article{1733,
abstract = {The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.},
author = {Cerny, Pavol and Chmelik, Martin and Henzinger, Thomas A and Radhakrishna, Arjun},
journal = {Theoretical Computer Science},
number = {3},
pages = {348 -- 363},
publisher = {Elsevier},
title = {{Interface simulation distances}},
doi = {10.1016/j.tcs.2014.08.019},
volume = {560},
year = {2014},
}
@inproceedings{2217,
abstract = {As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.
The contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem.},
author = {Henzinger, Thomas A and Otop, Jan},
booktitle = {Proceedings of the 17th international conference on Hybrid systems: computation and control},
location = {Berlin, Germany},
pages = {213 -- 222},
publisher = {Springer},
title = {{Model measuring for hybrid systems}},
doi = {10.1145/2562059.2562130},
year = {2014},
}
@inproceedings{1392,
abstract = {Fault-tolerant distributed algorithms play an important role in ensuring the reliability of many software applications. In this paper we consider distributed algorithms whose computations are organized in rounds. To verify the correctness of such algorithms, we reason about (i) properties (such as invariants) of the state, (ii) the transitions controlled by the algorithm, and (iii) the communication graph. We introduce a logic that addresses these points, and contains set comprehensions with cardinality constraints, function symbols to describe the local states of each process, and a limited form of quantifier alternation to express the verification conditions. We show its use in automating the verification of consensus algorithms. In particular, we give a semi-decision procedure for the unsatisfiability problem of the logic and identify a decidable fragment. We successfully applied our framework to verify the correctness of a variety of consensus algorithms tolerant to both benign faults (message loss, process crashes) and value faults (message corruption).},
author = {Dragoi, Cezara and Henzinger, Thomas A and Veith, Helmut and Widder, Josef and Zufferey, Damien},
location = {San Diego, USA},
pages = {161 -- 181},
publisher = {Springer},
title = {{A logic-based framework for verifying consensus algorithms}},
doi = {10.1007/978-3-642-54013-4_10},
volume = {8318},
year = {2014},
}
@inproceedings{2218,
abstract = {While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in the repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs.},
author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Tarrach, Thorsten},
isbn = {978-331908866-2},
location = {Vienna, Austria},
pages = {568 -- 584},
publisher = {Springer},
title = {{Regression-free synthesis for concurrency}},
doi = {10.1007/978-3-319-08867-9_38},
volume = {8559},
year = {2014},
}
@inproceedings{2167,
abstract = {Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing. In this paper, we study compositional properties of the ioco-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the ioco conformance relation, the resulting methodology can be applied to a broader class of systems.},
author = {Daca, Przemyslaw and Henzinger, Thomas A and Krenn, Willibald and Nickovic, Dejan},
booktitle = {IEEE 7th International Conference on Software Testing, Verification and Validation},
isbn = {978-1-4799-2255-0},
issn = {2159-4848},
location = {Cleveland, USA},
publisher = {IEEE},
title = {{Compositional specifications for IOCO testing}},
doi = {10.1109/ICST.2014.50},
year = {2014},
}
@inproceedings{1393,
abstract = {Probabilistic programs are usual functional or imperative programs with two added constructs: (1) the ability to draw values at random from distributions, and (2) the ability to condition values of variables in a program via observations. Models from diverse application areas such as computer vision, coding theory, cryptographic protocols, biology and reliability analysis can be written as probabilistic programs. Probabilistic inference is the problem of computing an explicit representation of the probability distribution implicitly specified by a probabilistic program. Depending on the application, the desired output from inference may vary-we may want to estimate the expected value of some function f with respect to the distribution, or the mode of the distribution, or simply a set of samples drawn from the distribution. In this paper, we describe connections this research area called \Probabilistic Programming" has with programming languages and software engineering, and this includes language design, and the static and dynamic analysis of programs. We survey current state of the art and speculate on promising directions for future research.},
author = {Gordon, Andrew and Henzinger, Thomas A and Nori, Aditya and Rajamani, Sriram},
booktitle = {Proceedings of the on Future of Software Engineering},
location = {Hyderabad, India},
pages = {167 -- 181},
publisher = {ACM},
title = {{Probabilistic programming}},
doi = {10.1145/2593882.2593900},
year = {2014},
}
@article{2233,
abstract = { A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, valuing a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by λi, where the discount factor λ is a fixed rational number greater than 1. The value of a word is the minimal value of the automaton runs on it. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, reflecting the assumption that earlier weights are more important than later weights. Unfortunately, determinization of NDAs, which is often essential in formal verification, is, in general, not possible. We provide positive news, showing that every NDA with an integral discount factor is determinizable. We complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: for every nonintegral rational discount factor λ, there is a nondeterminizable λ-NDA. We also prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. For general NDAs, we look into approximate determinization, which is always possible as the influence of a word's suffix decays. We show that the naive approach, of unfolding the automaton computations up to a sufficient level, is doubly exponential in the discount factor. We provide an alternative construction for approximate determinization, which is singly exponential in the discount factor, in the precision, and in the number of states. We also prove matching lower bounds, showing that the exponential dependency on each of these three parameters cannot be avoided. All our results hold equally for automata over finite words and for automata over infinite words. },
author = {Boker, Udi and Henzinger, Thomas A},
issn = {18605974},
journal = {Logical Methods in Computer Science},
number = {1},
publisher = {International Federation of Computational Logic},
title = {{Exact and approximate determinization of discounted-sum automata}},
doi = {10.2168/LMCS-10(1:10)2014},
volume = {10},
year = {2014},
}
@article{2187,
abstract = {Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if assumptions in the specification are violated. To overcome this, we define two robustness notions, combine them, and show how to enforce them in synthesis. The first notion applies to safety properties: If safety assumptions are violated temporarily, we require that the system recovers to normal operation with as few errors as possible. The second notion requires that, if liveness assumptions are violated, as many guarantees as possible should be fulfilled nevertheless. We present a synthesis procedure achieving this for the important class of GR(1) specifications, and establish complexity bounds. We also present an implementation of a special case of robustness, and show experimental results.},
author = {Bloem, Roderick and Chatterjee, Krishnendu and Greimel, Karin and Henzinger, Thomas A and Hofferek, Georg and Jobstmann, Barbara and Könighofer, Bettina and Könighofer, Robert},
journal = {Acta Informatica},
number = {3-4},
pages = {193 -- 220},
publisher = {Springer},
title = {{Synthesizing robust systems}},
doi = {10.1007/s00236-013-0191-5},
volume = {51},
year = {2014},
}
@misc{5415,
abstract = {Recently there has been a significant effort to add 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, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains. },
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
issn = {2664-1690},
pages = {27},
publisher = {IST Austria},
title = {{Nested weighted automata}},
doi = {10.15479/AT:IST-2014-170-v1-1},
year = {2014},
}
@article{2289,
abstract = {Formal verification aims to improve the quality of software by detecting errors before they do harm. At the basis of formal verification is the logical notion of correctness, which purports to capture whether or not a program behaves as desired. We suggest that the boolean partition of software into correct and incorrect programs falls short of the practical need to assess the behavior of software in a more nuanced fashion against multiple criteria. We therefore propose to introduce quantitative fitness measures for programs, specifically for measuring the function, performance, and robustness of reactive programs such as concurrent processes. This article describes the goals of the ERC Advanced Investigator Project QUAREM. The project aims to build and evaluate a theory of quantitative fitness measures for reactive models. Such a theory must strive to obtain quantitative generalizations of the paradigms that have been success stories in qualitative reactive modeling, such as compositionality, property-preserving abstraction and abstraction refinement, model checking, and synthesis. The theory will be evaluated not only in the context of software and hardware engineering, but also in the context of systems biology. In particular, we will use the quantitative reactive models and fitness measures developed in this project for testing hypotheses about the mechanisms behind data from biological experiments.},
author = {Henzinger, Thomas A},
journal = {Computer Science Research and Development},
number = {4},
pages = {331 -- 344},
publisher = {Springer},
title = {{Quantitative reactive modeling and verification}},
doi = {10.1007/s00450-013-0251-7},
volume = {28},
year = {2013},
}
@proceedings{2885,
abstract = {This volume contains the post-proceedings of the 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, MEMICS 2012, held in Znojmo, Czech Republic, in October, 2012. The 13 thoroughly revised papers were carefully selected out of 31 submissions and are presented together with 6 invited papers. The topics covered by the papers include: computer-aided analysis and verification, applications of game theory in computer science, networks and security, modern trends of graph theory in computer science, electronic systems design and testing, and quantum information processing.},
editor = {Kucera, Antonin and Henzinger, Thomas A and Nesetril, Jaroslav and Vojnar, Tomas and Antos, David},
location = {Znojmo, Czech Republic},
pages = {1 -- 228},
publisher = {Springer},
title = {{Mathematical and Engineering Methods in Computer Science}},
doi = {10.1007/978-3-642-36046-6},
volume = {7721},
year = {2013},
}
@misc{6440,
abstract = {In order to guarantee that each method of a data structure updates the logical state exactly once, al-most all non-blocking implementations employ Compare-And-Swap (CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods competing among themselves to update the same variable, the tail or the head, respectively, leading to high contention and poor scalability. Recent non-blocking queue implementations try to alleviate high contentionby increasing the number of contention points, all the while using CAS-based synchronization. Furthermore, obtaining a wait-free implementation with competition is achieved by additional synchronization which leads to further degradation of performance.In this paper we formalize the notion of competitiveness of a synchronizing statement which can beused as a measure for the scalability of concurrent implementations. We present a new queue implementation, the Speculative Pairing (SP) queue, which, as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead of CAS. We prove that the SP queue is linearizable and lock-free.We also show that replacing CAS with FAI leads to wait-freedom for dequeue methods without an adverse effect on performance. In fact, our experiments suggest that the SP queue can perform and scale better than the state-of-the-art queue implementations.},
author = {Henzinger, Thomas A and Payer, Hannes and Sezgin, Ali},
issn = {2664-1690},
pages = {23},
publisher = {IST Austria},
title = {{Replacing competition with cooperation to achieve scalable lock-free FIFO queues }},
doi = {10.15479/AT:IST-2013-124-v1-1},
year = {2013},
}
@inproceedings{1387,
abstract = {Choices made by nondeterministic word automata depend on both the past (the prefix of the word read so far) and the future (the suffix yet to be read). In several applications, most notably synthesis, the future is diverse or unknown, leading to algorithms that are based on deterministic automata. Hoping to retain some of the advantages of nondeterministic automata, researchers have studied restricted classes of nondeterministic automata. Three such classes are nondeterministic automata that are good for trees (GFT; i.e., ones that can be expanded to tree automata accepting the derived tree languages, thus whose choices should satisfy diverse futures), good for games (GFG; i.e., ones whose choices depend only on the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent deterministic automata). The theoretical properties and relative merits of the different classes are still open, having vagueness on whether they really differ from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also open is the possible succinctness of GFG and GFT automata compared to deterministic automata. We study these problems for ω-regular automata with all common acceptance conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction for GFG automata.},
author = {Boker, Udi and Kuperberg, Denis and Kupferman, Orna and Skrzypczak, Michał},
location = {Riga, Latvia},
number = {PART 2},
pages = {89 -- 100},
publisher = {Springer},
title = {{Nondeterminism in the presence of a diverse or unknown future}},
doi = {10.1007/978-3-642-39212-2_11},
volume = {7966},
year = {2013},
}
@inproceedings{2847,
abstract = {Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.},
author = {Bansal, Kshitij and Koskinen, Eric and Wies, Thomas and Zufferey, Damien},
editor = {Piterman, Nir and Smolka, Scott},
location = {Rome, Italy},
pages = {62 -- 77},
publisher = {Springer},
title = {{Structural Counter Abstraction}},
doi = {10.1007/978-3-642-36742-7_5},
volume = {7795},
year = {2013},
}
@article{2854,
abstract = {We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. First, we present a simple proof of the fact that in concurrent reachability games, for all ε>0, memoryless ε-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an ε-optimal strategy achieves the objective with probability within ε of the value of the game. In contrast to previous proofs of this fact, our proof is more elementary and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives. Finally, we present a strategy-improvement algorithm for turn-based stochastic games (where each player selects moves in turns) with safety objectives. Our algorithms yield sequences of player-1 strategies which ensure probabilities of winning that converge monotonically (from below) to the value of the game. © 2012 Elsevier Inc.},
author = {Chatterjee, Krishnendu and De Alfaro, Luca and Henzinger, Thomas A},
journal = {Journal of Computer and System Sciences},
number = {5},
pages = {640 -- 657},
publisher = {Elsevier},
title = {{Strategy improvement for concurrent reachability and turn based stochastic safety games}},
doi = {10.1016/j.jcss.2012.12.001},
volume = {79},
year = {2013},
}
@inproceedings{2328,
abstract = {Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on identifying 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 = {Henzinger, Thomas A and Sezgin, Ali and Vafeiadis, Viktor},
location = {Buenos Aires, Argentina},
pages = {242 -- 256},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Aspect-oriented linearizability proofs}},
doi = {10.1007/978-3-642-40184-8_18},
volume = {8052},
year = {2013},
}
@inproceedings{1376,
abstract = {We consider the distributed synthesis problem for temporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTL and our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3) Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan and Pavlogiannis, Andreas},
booktitle = {13th International Conference on Formal Methods in Computer-Aided Design},
location = {Portland, OR, United States},
pages = {18 -- 25},
publisher = {IEEE},
title = {{Distributed synthesis for LTL fragments}},
doi = {10.1109/FMCAD.2013.6679386},
year = {2013},
}
@misc{5406,
abstract = {We consider the distributed synthesis problem fortemporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTLand our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3)Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan and Pavlogiannis, Andreas},
issn = {2664-1690},
pages = {11},
publisher = {IST Austria},
title = {{Distributed synthesis for LTL Fragments}},
doi = {10.15479/AT:IST-2013-130-v1-1},
year = {2013},
}
@inproceedings{2445,
abstract = {We develop program synthesis techniques that can help programmers fix concurrency-related bugs. We make two new contributions to synthesis for concurrency, the first improving the efficiency of the synthesized code, and the second improving the efficiency of the synthesis procedure itself. The first contribution is to have the synthesis procedure explore a variety of (sequential) semantics-preserving program transformations. Classically, only one such transformation has been considered, namely, the insertion of synchronization primitives (such as locks). Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. The second contribution is to speed up the counterexample-guided removal of concurrency bugs within the synthesis procedure by considering partial-order traces (instead of linear traces) as counterexamples. A partial-order error trace represents a set of linear (interleaved) traces of a concurrent program all of which lead to the same error. By eliminating a partial-order error trace, we eliminate in a single iteration of the synthesis procedure all linearizations of the partial-order trace. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers.},
author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Tarrach, Thorsten},
location = {St. Petersburg, Russia},
pages = {951 -- 967},
publisher = {Springer},
title = {{Efficient synthesis for concurrency by semantics-preserving transformations}},
doi = {10.1007/978-3-642-39799-8_68},
volume = {8044},
year = {2013},
}
@inproceedings{2298,
abstract = {We present a shape analysis for programs that manipulate overlaid data structures which share sets of objects. The abstract domain contains Separation Logic formulas that (1) combine a per-object separating conjunction with a per-field separating conjunction and (2) constrain a set of variables interpreted as sets of objects. The definition of the abstract domain operators is based on a notion of homomorphism between formulas, viewed as graphs, used recently to define optimal decision procedures for fragments of the Separation Logic. Based on a Frame Rule that supports the two versions of the separating conjunction, the analysis is able to reason in a modular manner about non-overlaid data structures and then, compose information only at a few program points, e.g., procedure returns. We have implemented this analysis in a prototype tool and applied it on several interesting case studies that manipulate overlaid and nested linked lists.
},
author = {Dragoi, Cezara and Enea, Constantin and Sighireanu, Mihaela},
location = {Seattle, WA, United States},
pages = {150 -- 171},
publisher = {Springer},
title = {{Local shape analysis for overlaid data structures}},
doi = {10.1007/978-3-642-38856-9_10},
volume = {7935},
year = {2013},
}
@inproceedings{2301,
abstract = {We describe the design and implementation of P, a domain-specific language to write asynchronous event driven code. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be tested using model checking techniques. P allows the programmer to specify the environment, used to "close" the system during testing, as nondeterministic ghost machines. Ghost machines are erased during compilation to executable code; a type system ensures that the erasure is semantics preserving. The P language is designed so that a P program can be checked for responsiveness-the ability to handle every event in a timely manner. By default, a machine needs to handle every event that arrives in every state. But handling every event in every state is impractical. The language provides a notion of deferred events where the programmer can annotate when she wants to delay processing an event. The default safety checker looks for presence of unhan-dled events. The language also provides default liveness checks that an event cannot be potentially deferred forever. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8. The resulting driver is more reliable and performs better than its prior incarnation (which did not use P); we have more confidence in the robustness of its design due to the language abstractions and verification provided by P.},
author = {Desai, Ankush and Gupta, Vivek and Jackson, Ethan and Qadeer, Shaz and Rajamani, Sriram and Zufferey, Damien},
booktitle = {Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation},
location = {Seattle, WA, United States},
pages = {321 -- 331},
publisher = {ACM},
title = {{P: Safe asynchronous event-driven programming}},
doi = {10.1145/2491956.2462184},
year = {2013},
}
@inproceedings{2243,
abstract = {We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NEXPTIME.},
author = {Michaliszyn, Jakub and Otop, Jan},
location = {Torino, Italy},
pages = {563 -- 577},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Elementary modal logics over transitive structures}},
doi = {10.4230/LIPIcs.CSL.2013.563},
volume = {23},
year = {2013},
}