@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{1595,
abstract = {A drawing of a graph G is radial if the vertices of G are placed on concentric circles C1, . . . , Ck with common center c, and edges are drawn radially: every edge intersects every circle centered at c at most once. G is radial planar if it has a radial embedding, that is, a crossing- free radial drawing. If the vertices of G are ordered or partitioned into ordered levels (as they are for leveled graphs), we require that the assignment of vertices to circles corresponds to the given ordering or leveling. We show that a graph G is radial planar if G has a radial drawing in which every two edges cross an even number of times; the radial embedding has the same leveling as the radial drawing. In other words, we establish the weak variant of the Hanani-Tutte theorem for radial planarity. This generalizes a result by Pach and Tóth.},
author = {Fulek, Radoslav and Pelsmajer, Michael and Schaefer, Marcus},
location = {Los Angeles, CA, USA},
pages = {99 -- 110},
publisher = {Springer},
title = {{Hanani-Tutte for radial planarity}},
doi = {10.1007/978-3-319-27261-0_9},
volume = {9411},
year = {2015},
}
@inproceedings{1596,
abstract = {Let C={C1,...,Cn} denote a collection of translates of a regular convex k-gon in the plane with the stacking order. The collection C forms a visibility clique if for everyi < j the intersection Ci and (Ci ∩ Cj)\⋃i<l<jCl =∅.elements that are stacked between them, i.e., We show that if C forms a visibility clique its size is bounded from above by O(k4) thereby improving the upper bound of 22k from the aforementioned paper. We also obtain an upper bound of 22(k/2)+2 on the size of a visibility clique for homothetes of a convex (not necessarily regular) k-gon.},
author = {Fulek, Radoslav and Radoičić, Radoš},
location = {Los Angeles, CA, United States},
pages = {373 -- 379},
publisher = {Springer},
title = {{Vertical visibility among parallel polygons in three dimensions}},
doi = {10.1007/978-3-319-27261-0_31},
volume = {9411},
year = {2015},
}
@article{1598,
abstract = {We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives, and examine the problem of computing the set of almost-sure winning vertices such that the objective can be ensured with probability 1 from these vertices. We study for the first time the average-case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average-case running time is linear (as compared to the worst-case linear number of iterations and quadratic time complexity). Second, for the average-case analysis over all MDPs we show that the expected number of iterations is constant and the average-case running time is linear (again as compared to the worst-case linear number of iterations and quadratic time complexity). Finally we also show that when all MDPs are equally likely, the probability that the classical algorithm requires more than a constant number of iterations is exponentially small.},
author = {Chatterjee, Krishnendu and Joglekar, Manas and Shah, Nisarg},
journal = {Theoretical Computer Science},
number = {3},
pages = {71 -- 89},
publisher = {Elsevier},
title = {{Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives}},
doi = {10.1016/j.tcs.2015.01.050},
volume = {573},
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},
}
@article{1602,
abstract = {Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks.},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas and Goyal, Prateesh},
journal = {ACM SIGPLAN Notices},
location = {Mumbai, India},
number = {1},
pages = {97 -- 109},
publisher = {ACM},
title = {{Faster algorithms for algebraic path properties in recursive state machines with constant treewidth}},
doi = {10.1145/2676726.2676979},
volume = {50},
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},
}
@article{1604,
abstract = {We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs.},
author = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Velner, Yaron},
isbn = {978-1-4503-3300-9},
journal = {Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT },
location = {Mumbai, India},
number = {1},
pages = {539 -- 551},
publisher = {ACM},
title = {{Quantitative interprocedural analysis}},
doi = {10.1145/2676726.2676968},
volume = {50},
year = {2015},
}
@inproceedings{1605,
abstract = {Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.},
author = {Bogomolov, Sergiy and Schilling, Christian and Bartocci, Ezio and Batt, Grégory and Kong, Hui and Grosu, Radu},
location = {Haifa, Israel},
pages = {19 -- 35},
publisher = {Springer},
title = {{Abstraction-based parameter synthesis for multiaffine systems}},
doi = {10.1007/978-3-319-26287-1_2},
volume = {9434},
year = {2015},
}
@inproceedings{1606,
abstract = {In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.},
author = {Nguyen, Luan and Schilling, Christian and Bogomolov, Sergiy and Johnson, Taylor},
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},
}