TY - JOUR AB - Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks. AU - Bogomolov, Sergiy AU - Forets, Marcelo AU - Frehse, Goran AU - Potomkin, Kostiantyn AU - Schilling, Christian ID - 8790 IS - 11 JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems SN - 02780070 TI - Reachability analysis of linear hybrid systems via block decomposition VL - 39 ER - TY - JOUR AB - In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve. AU - Avni, Guy AU - Ibsen-Jensen, Rasmus AU - Tkadlec, Josef ID - 9197 IS - 02 JF - Proceedings of the AAAI Conference on Artificial Intelligence SN - 2159-5399 TI - All-pay bidding games on graphs VL - 34 ER - TY - CONF AB - We introduce the monitoring of trace properties under assumptions. An assumption limits the space of possible traces that the monitor may encounter. An assumption may result from knowledge about the system that is being monitored, about the environment, or about another, connected monitor. We define monitorability under assumptions and study its theoretical properties. In particular, we show that for every assumption A, the boolean combinations of properties that are safe or co-safe relative to A are monitorable under A. We give several examples and constructions on how an assumption can make a non-monitorable property monitorable, and how an assumption can make a monitorable property monitorable with fewer resources, such as integer registers. AU - Henzinger, Thomas A AU - Sarac, Naci E ID - 8623 SN - 0302-9743 T2 - Runtime Verification TI - Monitorability under assumptions VL - 12399 ER - TY - CONF AB - This paper presents a foundation for refining concurrent programs with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the Civl verifier. AU - Kragl, Bernhard AU - Qadeer, Shaz AU - Henzinger, Thomas A ID - 8195 SN - 0302-9743 T2 - Computer Aided Verification TI - Refinement for structured concurrent programs VL - 12224 ER - TY - CONF AB - Asynchronous programs are notoriously difficult to reason about because they spawn computation tasks which take effect asynchronously in a nondeterministic way. Devising inductive invariants for such programs requires understanding and stating complex relationships between an unbounded number of computation tasks in arbitrarily long executions. In this paper, we introduce inductive sequentialization, a new proof rule that sidesteps this complexity via a sequential reduction, a sequential program that captures every behavior of the original program up to reordering of coarse-grained commutative actions. A sequential reduction of a concurrent program is easy to reason about since it corresponds to a simple execution of the program in an idealized synchronous environment, where processes act in a fixed order and at the same speed. We have implemented and integrated our proof rule in the CIVL verifier, allowing us to provably derive fine-grained implementations of asynchronous programs. We have successfully applied our proof rule to a diverse set of message-passing protocols, including leader election protocols, two-phase commit, and Paxos. AU - Kragl, Bernhard AU - Enea, Constantin AU - Henzinger, Thomas A AU - Mutluergil, Suha Orhun AU - Qadeer, Shaz ID - 8012 SN - 9781450376136 T2 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation TI - Inductive sequentialization of asynchronous programs ER -