@article{6752,
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. The following bidding rule was previously defined and called Richman bidding. Both players have separate budgets, which sum up to 1. In each turn, a bidding takes place: Both players submit bids simultaneously, where a bid is legal if it does not exceed the available budget, and the higher bidder pays his bid to the other player and moves the token. The central question studied in bidding games is a necessary and sufficient initial budget for winning the game: a threshold budget in a vertex is a value t ∈ [0, 1] such that if Player 1’s budget exceeds t, he can win the game; and if Player 2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously shown to exist in every vertex of a reachability game, which have an interesting connection with random-turn games—a sub-class of simple stochastic games in which the player who moves is chosen randomly. We show the existence of threshold budgets for a qualitative class of infinite-duration games, namely parity games, and a quantitative class, namely mean-payoff games. The key component of the proof is a quantitative solution to strongly connected mean-payoff bidding games in which we extend the connection with random-turn games to these games, and construct explicit optimal strategies for both players.},
author = {Avni, Guy and Henzinger, Thomas A and Chonev, Ventsislav K},
issn = {1557735X},
journal = {Journal of the ACM},
number = {4},
publisher = {ACM},
title = {{Infinite-duration bidding games}},
doi = {10.1145/3340295},
volume = {66},
year = {2019},
}
@inproceedings{6462,
abstract = {A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles.},
author = {Avni, Guy and Bloem, Roderick and Chatterjee, Krishnendu and Henzinger, Thomas A and Konighofer, Bettina and Pranger, Stefan},
booktitle = {31st International Conference on Computer-Aided Verification},
isbn = {9783030255398},
issn = {0302-9743},
location = {New York, NY, United States},
pages = {630--649},
publisher = {Springer},
title = {{Run-time optimization for learned controllers through quantitative games}},
doi = {10.1007/978-3-030-25540-4_36},
volume = {11561},
year = {2019},
}
@inproceedings{6493,
abstract = {We present two algorithmic approaches for synthesizing linear hybrid automata from experimental data. Unlike previous approaches, our algorithms work without a template and generate an automaton with nondeterministic guards and invariants, and with an arbitrary number and topology of modes. They thus construct a succinct model from the data and provide formal guarantees. In particular, (1) the generated automaton can reproduce the data up to a specified tolerance and (2) the automaton is tight, given the first guarantee. Our first approach encodes the synthesis problem as a logical formula in the theory of linear arithmetic, which can then be solved by an SMT solver. This approach minimizes the number of modes in the resulting model but is only feasible for limited data sets. To address scalability, we propose a second approach that does not enforce to find a minimal model. The algorithm constructs an initial automaton and then iteratively extends the automaton based on processing new data. Therefore the algorithm is well-suited for online and synthesis-in-the-loop applications. The core of the algorithm is a membership query that checks whether, within the specified tolerance, a given data set can result from the execution of a given automaton. We solve this membership problem for linear hybrid automata by repeated reachability computations. We demonstrate the effectiveness of the algorithm on synthetic data sets and on cardiac-cell measurements.},
author = {Garcia Soto, Miriam and Henzinger, Thomas A and Schilling, Christian and Zeleznik, Luka},
booktitle = {31st International Conference on Computer-Aided Verification},
isbn = {9783030255398},
issn = {0302-9743},
keyword = {Synthesis, Linear hybrid automaton, Membership},
location = {New York City, NY, USA},
pages = {297--314},
publisher = {Springer},
title = {{Membership-based synthesis of linear hybrid automata}},
doi = {10.1007/978-3-030-25540-4_16},
volume = {11561},
year = {2019},
}
@inproceedings{6885,
abstract = {A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open. },
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
location = {Amsterdam, Netherlands},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Long-run average behavior of vector addition systems with states}},
doi = {10.4230/LIPICS.CONCUR.2019.27},
volume = {140},
year = {2019},
}
@inproceedings{7232,
abstract = {We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. },
author = {Ferrere, Thomas and Maler, Oded and Nickovic, Dejan},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
isbn = {9783030296612},
issn = {16113349},
location = {Amsterdam, The Netherlands},
pages = {59--75},
publisher = {Springer Nature},
title = {{Mixed-time signal temporal logic}},
doi = {10.1007/978-3-030-29662-9_4},
volume = {11750},
year = {2019},
}
@inproceedings{7453,
abstract = {We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement.},
author = {Alur, Rajeev and Giacobbe, Mirco and Henzinger, Thomas A and Larsen, Kim G. and Mikučionis, Marius},
booktitle = {Computing and Software Science},
isbn = {9783319919072},
issn = {0302-9743},
pages = {452--477},
publisher = {Springer Nature},
title = {{Continuous-time models for system design and analysis}},
doi = {10.1007/978-3-319-91908-9_22},
volume = {10000},
year = {2019},
}
@inproceedings{6886,
abstract = {In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets. },
author = {Aghajohari, Milad and Avni, Guy and Henzinger, Thomas A},
location = {Amsterdam, Netherlands},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Determinacy in discrete-bidding infinite-duration games}},
doi = {10.4230/LIPICS.CONCUR.2019.20},
volume = {140},
year = {2019},
}
@inproceedings{299,
abstract = {We introduce in this paper AMT 2.0 , a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended Signal Temporal Logic (xSTL), which integrates Timed Regular Expressions (TRE) within Signal Temporal Logic (STL). The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal.},
author = {Nickovic, Dejan and Lebeltel, Olivier and Maler, Oded and Ferrere, Thomas and Ulus, Dogan},
editor = {Beyer, Dirk and Huisman, Marieke},
location = {Thessaloniki, Greece},
pages = {303 -- 319},
publisher = {Springer},
title = {{AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic}},
doi = {10.1007/978-3-319-89963-3_18},
volume = {10806},
year = {2018},
}
@article{434,
abstract = {In this paper, we present a formal model-driven design approach to establish a safety-assured implementation of multifunction vehicle bus controller (MVBC), which controls the data transmission among the devices of the vehicle. First, the generic models and safety requirements described in International Electrotechnical Commission Standard 61375 are formalized as time automata and timed computation tree logic formulas, respectively. With model checking tool Uppaal, we verify whether or not the constructed timed automata satisfy the formulas and several logic inconsistencies in the original standard are detected and corrected. Then, we apply the code generation tool Times to generate C code from the verified model, which is later synthesized into a real MVBC chip, with some handwriting glue code. Furthermore, the runtime verification tool RMOR is applied on the integrated code, to verify some safety requirements that cannot be formalized on the timed automata. For evaluation, we compare the proposed approach with existing MVBC design methods, such as BeagleBone, Galsblock, and Simulink. Experiments show that more ambiguousness or bugs in the standard are detected during Uppaal verification, and the generated code of Times outperforms the C code generated by others in terms of the synthesized binary code size. The errors in the standard have been confirmed and the resulting MVBC has been deployed in the real train communication network.},
author = {Jiang, Yu and Liu, Han and Song, Huobing and Kong, Hui and Wang, Rui and Guan, Yong and Sha, Lui},
journal = {IEEE Transactions on Intelligent Transportation Systems},
number = {10},
pages = {3320 -- 3333},
publisher = {IEEE},
title = {{Safety-assured model-driven design of the multifunction vehicle bus controller}},
doi = {10.1109/TITS.2017.2778077},
volume = {19},
year = {2018},
}
@inproceedings{5788,
abstract = {In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner or payoff of the game. Such games are central in formal verification since they model the interaction between a non-terminating system and its environment. We study bidding games in which the players bid for the right to move the token. Two bidding rules have been defined. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the “bank” rather than the other player. While poorman reachability games have been studied before, we present, for the first time, results on infinite-duration poorman games. A central quantity in these games is the ratio between the two players’ initial budgets. The questions we study concern a necessary and sufficient ratio with which a player can achieve a goal. For reachability objectives, such threshold ratios are known to exist for both bidding rules. We show that the properties of poorman reachability games extend to complex qualitative objectives such as parity, similarly to the Richman case. Our most interesting results concern quantitative poorman games, namely poorman mean-payoff games, where we construct optimal strategies depending on the initial ratio, by showing a connection with random-turn based games. The connection in itself is interesting, because it does not hold for reachability poorman games. We also solve the complexity problems that arise in poorman bidding games.},
author = {Avni, Guy and Henzinger, Thomas A and Ibsen-Jensen, Rasmus},
isbn = {9783030046118},
issn = {03029743},
location = {Oxford, UK},
pages = {21--36},
publisher = {Springer},
title = {{Infinite-duration poorman-bidding games}},
doi = {10.1007/978-3-030-04612-5_2},
volume = {11316},
year = {2018},
}