@inproceedings{1605,
abstract = {Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.},
author = {Bogomolov, Sergiy and Schilling, Christian and Bartocci, Ezio and Batt, Grégory and Kong, Hui and Grosu, Radu},
location = {Haifa, Israel},
pages = {19 -- 35},
publisher = {Springer},
title = {{Abstraction-based parameter synthesis for multiaffine systems}},
doi = {10.1007/978-3-319-26287-1_2},
volume = {9434},
year = {2015},
}
@inproceedings{1606,
abstract = {In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.},
author = {Nguyen, Luan and Schilling, Christian and Bogomolov, Sergiy and Johnson, Taylor},
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{1607,
abstract = {We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
location = {San Francisco, CA, USA},
pages = {140 -- 157},
publisher = {Springer},
title = {{Faster algorithms for quantitative verification in constant treewidth graphs}},
doi = {10.1007/978-3-319-21690-4_9},
volume = {9206},
year = {2015},
}
@inproceedings{1609,
abstract = {The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is “constructed from scratch” rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP ∩ coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Vardi, Moshe},
location = {Kyoto, Japan},
pages = {108 -- 120},
publisher = {Springer},
title = {{The complexity of synthesis from probabilistic components}},
doi = {10.1007/978-3-662-47666-6_9},
volume = {9135},
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},
}