@article{1407, 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 all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated 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}, journal = {Nonlinear Analysis: Hybrid Systems}, number = {2}, pages = {230 -- 253}, publisher = {Elsevier}, title = {{Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games}}, doi = {10.1016/j.nahs.2016.04.006}, volume = {23}, year = {2017}, } @inproceedings{941, abstract = {Recently there has been a proliferation of automated program repair (APR) techniques, targeting various programming languages. Such techniques can be generally classified into two families: syntactic- and semantics-based. Semantics-based APR, on which we focus, typically uses symbolic execution to infer semantic constraints and then program synthesis to construct repairs conforming to them. While syntactic-based APR techniques have been shown successful on bugs in real-world programs written in both C and Java, semantics-based APR techniques mostly target C programs. This leaves empirical comparisons of the APR families not fully explored, and developers without a Java-based semantics APR technique. We present JFix, a semantics-based APR framework that targets Java, and an associated Eclipse plugin. JFix is implemented atop Symbolic PathFinder, a well-known symbolic execution engine for Java programs. It extends one particular APR technique (Angelix), and is designed to be sufficiently generic to support a variety of such techniques. We demonstrate that semantics-based APR can indeed efficiently and effectively repair a variety of classes of bugs in large real-world Java programs. This supports our claim that the framework can both support developers seeking semantics-based repair of bugs in Java programs, as well as enable larger scale empirical studies comparing syntactic- and semantics-based APR targeting Java. The demonstration of our tool is available via the project website at: https://xuanbachle.github.io/semanticsrepair/ }, author = {Le, Xuan and Chu, Duc Hiep and Lo, David and Le Goues, Claire and Visser, Willem}, booktitle = {Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis}, location = {Santa Barbara, CA, United States}, pages = {376 -- 379 }, publisher = {ACM}, title = {{JFIX: Semantics-based repair of Java programs via symbolic PathFinder}}, doi = {10.1145/3092703.3098225}, year = {2017}, } @inproceedings{942, abstract = {A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration-based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs. }, author = {Le, Xuan and Chu, Duc Hiep and Lo, David and Le Goues, Claire and Visser, Willem}, isbn = {978-145035105-8}, location = {Paderborn, Germany}, pages = {593 -- 604}, publisher = {ACM}, title = {{S3: Syntax- and semantic-guided repair synthesis via programming by examples}}, doi = {10.1145/3106237.3106309}, volume = {F130154}, year = {2017}, } @inproceedings{950, abstract = {Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\in [0,1] such that if\PO's budget exceeds $t$, he can win the game, and if\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. }, author = {Avni, Guy and Henzinger, Thomas A and Chonev, Ventsislav K}, issn = {1868-8969}, location = {Berlin, Germany}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Infinite-duration bidding games}}, doi = {10.4230/LIPIcs.CONCUR.2017.21}, volume = {85}, year = {2017}, } @inproceedings{962, abstract = {We present a new algorithm for model counting of a class of string constraints. In addition to the classic operation of concatenation, our class includes some recursively defined operations such as Kleene closure, and replacement of substrings. Additionally, our class also includes length constraints on the string expressions, which means, by requiring reasoning about numbers, that we face a multi-sorted logic. In the end, our string constraints are motivated by their use in programming for web applications. Our algorithm comprises two novel features: the ability to use a technique of (1) partial derivatives for constraints that are already in a solved form, i.e. a form where its (string) satisfiability is clearly displayed, and (2) non-progression, where cyclic reasoning in the reduction process may be terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally compare our model counter with two recent works on model counting of similar constraints, SMC [18] and ABC [5], to demonstrate its superior performance.}, author = {Trinh, Minh and Chu, Duc Hiep and Jaffar, Joxan}, editor = {Majumdar, Rupak and Kunčak, Viktor}, issn = {03029743}, location = {Heidelberg, Germany}, pages = {399 -- 418}, publisher = {Springer}, title = {{Model counting for recursively-defined strings}}, doi = {10.1007/978-3-319-63390-9_21}, volume = {10427}, year = {2017}, } @inproceedings{963, abstract = {Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertex. The cost of traversing an edge depends on the number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in defining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, the traversal of the network involves an inherent delay, and so sharing and congestion of resources crucially depends on time. We study timed network games , which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. In addition, each edge has a guard, describing time intervals in which the edge can be traversed, forcing the players to spend time on vertices. Unlike earlier work that add a time component to network games, the time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We study properties of timed network games with cost-sharing or congestion cost functions: their stability, equilibrium inefficiency, and complexity. In particular, we show that the answer to the question whether we can restrict attention to boundary strategies, namely ones in which edges are traversed only at the boundaries of guards, is mixed. }, author = {Avni, Guy and Guha, Shibashis and Kupferman, Orna}, issn = {18688969}, location = {Aalborg, Denmark}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Timed network games with clocks}}, doi = {10.4230/LIPIcs.MFCS.2017.37}, volume = {83}, year = {2017}, } @inproceedings{1003, abstract = {Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology.}, author = {Avni, Guy and Guha, Shibashis and Kupferman, Orna}, issn = {10450823}, location = {Melbourne, Australia}, pages = {70 -- 76}, publisher = {AAAI Press}, title = {{An abstraction-refinement methodology for reasoning about network games}}, doi = {10.24963/ijcai.2017/11}, year = {2017}, } @inproceedings{1011, abstract = {Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.}, author = {Chatterjee, Krishnendu and Kragl, Bernhard and Mishra, Samarth and Pavlogiannis, Andreas}, editor = {Yang, Hongseok}, issn = {03029743}, location = {Uppsala, Sweden}, pages = {287 -- 313}, publisher = {Springer}, title = {{Faster algorithms for weighted recursive state machines}}, doi = {10.1007/978-3-662-54434-1_11}, volume = {10201}, year = {2017}, } @article{10418, abstract = {We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. "super-martingales") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.}, author = {Mciver, Annabelle and Morgan, Carroll and Kaminski, Benjamin Lucien and Katoen, Joost P}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, location = {Los Angeles, CA, United States}, number = {POPL}, publisher = {Association for Computing Machinery}, title = {{A new proof rule for almost-sure termination}}, doi = {10.1145/3158121}, volume = {2}, year = {2017}, } @article{1196, 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; robustness problems that measure how much a model can be perturbed without violating the specification; and parameter synthesis for hybrid systems. We show that for automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular branching-time, and (c) hybrid specifications, the model-measuring problem can be solved.We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for word, tree, and hybrid automata by the . optimal-value question for the weighted versions of these automata. For automata over words and trees, we consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. For hybrid automata, we consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete) weighted automata.We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications. Further, we propose the modeling framework for model measuring to ease the specification and reduce the likelihood of errors in modeling.Finally, we present a variant of the model-measuring problem, called the . model-repair problem. The model-repair problem applies to models that do not satisfy the specification; it can be used to derive restrictions, under which the model satisfies the specification, i.e., to repair the model.}, author = {Henzinger, Thomas A and Otop, Jan}, journal = {Nonlinear Analysis: Hybrid Systems}, pages = {166 -- 190}, publisher = {Elsevier}, title = {{Model measuring for discrete and hybrid systems}}, doi = {10.1016/j.nahs.2016.09.001}, volume = {23}, year = {2017}, } @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{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{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}, } @phdthesis{1130, abstract = {In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion statements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver benchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency.}, author = {Tarrach, Thorsten}, issn = {2663-337X}, pages = {151}, publisher = {Institute of Science and Technology Austria}, title = {{Automatic synthesis of synchronisation primitives for concurrent programs}}, doi = {10.15479/at:ista:1130}, year = {2016}, } @inproceedings{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{1135, abstract = {Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM.}, author = {Avni, Guy and Guha, Shibashis and Rodríguez Navas, Guillermo}, booktitle = {Proceedings of the 13th International Conference on Embedded Software }, location = {Pittsburgh, PA, USA}, publisher = {ACM}, title = {{Synthesizing time triggered schedules for switched networks with faulty links}}, doi = {10.1145/2968478.2968499}, 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}, } @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{1166, abstract = {POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.}, author = {Chatterjee, Krishnendu and Chmelik, Martin and Davies, Jessica}, booktitle = {Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence}, location = {Phoenix, AZ, USA}, pages = {3225 -- 3232}, publisher = {AAAI Press}, title = {{A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps}}, volume = {2016}, year = {2016}, }