@inproceedings{6565,
abstract = {In this paper, we address the problem of synthesizing periodic switching controllers for stabilizing a family of linear systems. Our broad approach consists of constructing a finite game graph based on the family of linear systems such that every winning strategy on the game graph corresponds to a stabilizing switching controller for the family of linear systems. The construction of a (finite) game graph, the synthesis of a winning strategy and the extraction of a stabilizing controller are all computationally feasible. We illustrate our method on an example.},
author = {Kundu, Atreyee and Garcia Soto, Miriam and Prabhakar, Pavithra},
booktitle = {5th Indian Control Conference Proceedings},
isbn = {978-153866246-5},
location = {Delhi, India},
publisher = {IEEE},
title = {{Formal synthesis of stabilizing controllers for periodically controlled linear switched systems}},
doi = {10.1109/INDIANCC.2019.8715598},
year = {2019},
}
@phdthesis{6894,
abstract = {Hybrid automata combine finite automata and dynamical systems, and model the interaction of digital with physical systems. Formal analysis that can guarantee the safety of all behaviors or rigorously witness failures, while unsolvable in general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking, assisted theorem proving.
Nevertheless, very few methods have addressed the time-unbounded reachability analysis of hybrid automata and, for current sound and automatic tools, scalability remains critical. We develop methods for the polyhedral abstraction of hybrid automata, which construct coarse overapproximations and tightens them incrementally, in a CEGAR fashion. We use template polyhedra, i.e., polyhedra whose facets are normal to a given set of directions.
While, previously, directions were given by the user, we introduce (1) the first method
for computing template directions from spurious counterexamples, so as to generalize and
eliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid
automata with (possibly non-linear) convex constraints on derivatives only, while for linear
ODE requires further abstraction. Specifically, we introduce (2) the conic abstractions,
which, partitioning the state space into appropriate (possibly non-uniform) cones, divide
curvy trajectories into relatively straight sections, suitable for polyhedral abstractions.
Finally, we introduce (3) space-time interpolation, which, combining interval arithmetic
and template refinement, computes appropriate (possibly non-uniform) time partitioning
and template directions along spurious trajectories, so as to eliminate them.
We obtain sound and automatic methods for the reachability analysis over dense
and unbounded time of convex hybrid automata and hybrid automata with linear ODE.
We build prototype tools and compare—favorably—our methods against the respective
state-of-the-art tools, on several benchmarks.},
author = {Giacobbe, Mirco},
issn = {2663-337X},
pages = {132},
publisher = {IST Austria},
title = {{Automatic time-unbounded reachability analysis of hybrid systems}},
doi = {10.15479/AT:ISTA:6894},
year = {2019},
}
@inproceedings{6035,
abstract = {We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.},
author = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
booktitle = {Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control},
isbn = {9781450362825},
keyword = {reachability analysis, hybrid systems, lazy computation},
location = {Montreal, QC, Canada},
pages = {39--44},
publisher = {ACM},
title = {{JuliaReach: A toolbox for set-based reachability}},
doi = {10.1145/3302504.3311804},
volume = {22},
year = {2019},
}
@inproceedings{6042,
abstract = {Static program analyzers are increasingly effective in checking correctness properties of programs and reporting any errors found, often in the form of error traces. However, developers still spend a significant amount of time on debugging. This involves processing long error traces in an effort to localize a bug to a relatively small part of the program and to identify its cause. In this paper, we present a technique for automated fault localization that, given a program and an error trace, efficiently narrows down the cause of the error to a few statements. These statements are then ranked in terms of their suspiciousness. Our technique relies only on the semantics of the given program and does not require any test cases or user guidance. In experiments on a set of C benchmarks, we show that our technique is effective in quickly isolating the cause of error while out-performing other state-of-the-art fault-localization techniques.},
author = {Christakis, Maria and Heizmann, Matthias and Mansur, Muhammad Numair and Schilling, Christian and Wüstholz, Valentin},
booktitle = {25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems },
location = {Prague, Czech Republic},
pages = {226--243},
publisher = {Springer Nature},
title = {{Semantic fault localization and suspiciousness ranking}},
doi = {10.1007/978-3-030-17462-0_13},
volume = {11427},
year = {2019},
}
@inproceedings{6888,
abstract = {In this paper, we design novel liquid time-constant recurrent neural networks for robotic control, inspired by the brain of the nematode, C. elegans. In the worm's nervous system, neurons communicate through nonlinear time-varying synaptic links established amongst them by their particular wiring structure. This property enables neurons to express liquid time-constants dynamics and therefore allows the network to originate complex behaviors with a small number of neurons. We identify neuron-pair communication motifs as design operators and use them to configure compact neuronal network structures to govern sequential robotic tasks. The networks are systematically designed to map the environmental observations to motor actions, by their hierarchical topology from sensory neurons, through recurrently-wired interneurons, to motor neurons. The networks are then parametrized in a supervised-learning scheme by a search-based algorithm. We demonstrate that obtained networks realize interpretable dynamics. We evaluate their performance in controlling mobile and arm robots, and compare their attributes to other artificial neural network-based control agents. Finally, we experimentally show their superior resilience to environmental noise, compared to the existing machine learning-based methods.},
author = {Lechner, Mathias and Hasani, Ramin and Zimmer, Manuel and Henzinger, Thomas A and Grosu, Radu},
booktitle = {Proceedings - IEEE International Conference on Robotics and Automation},
isbn = {9781538660270},
location = {Montreal, QC, Canada},
publisher = {IEEE},
title = {{Designing worm-inspired neural networks for interpretable robotic control}},
doi = {10.1109/icra.2019.8793840},
volume = {2019-May},
year = {2019},
}
@inproceedings{6428,
abstract = {Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposedas a language to specify and monitor the correctness of CPS relativeto formalized requirements. Incorporating STL into a developmentprocess enables designers to automatically monitor and diagnosetraces, compute robustness estimates based on requirements, andperform requirement falsification, leading to productivity gains inverification and validation activities; however, in its current formSTL is agnostic to the input/output classification of signals, andthis negatively impacts the relevance of the analysis results.In this paper we propose to make the interface explicit in theSTL language by introducing input/output signal declarations. Wethen define new measures of input vacuity and output robustnessthat better reflect the nature of the system and the specification in-tent. The resulting framework, which we call interface-aware signaltemporal logic (IA-STL), aids verification and validation activities.We demonstrate the benefits of IA-STL on several CPS analysisactivities: (1) robustness-driven sensitivity analysis, (2) falsificationand (3) fault localization. We describe an implementation of our en-hancement to STL and associated notions of robustness and vacuityin a prototype extension of Breach, a MATLAB®/Simulink®toolboxfor CPS verification and validation. We explore these methodologi-cal improvements and evaluate our results on two examples fromthe automotive domain: a benchmark powertrain control systemand a hydrogen fuel cell system.},
author = {Ferrere, Thomas and Nickovic, Dejan and Donzé, Alexandre and Ito, Hisahiro and Kapinski, James},
booktitle = {Proceedings of the 2019 22nd ACM International Conference on Hybrid Systems: Computation and Control},
isbn = {9781450362825},
location = {Montreal, Canada},
pages = {57--66},
publisher = {ACM},
title = {{Interface-aware signal temporal logic}},
doi = {10.1145/3302504.3311800},
year = {2019},
}
@inproceedings{6884,
abstract = {In two-player games on graphs, the players move a token through a graph to produce a finite or infinite path, which determines the qualitative winner or quantitative payoff of the game. We study bidding games in which the players bid for the right to move the token. Several bidding rules were studied previously. 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. Taxman bidding spans the spectrum between Richman and poorman bidding. They are parameterized by a constant tau in [0,1]: portion tau of the winning bid is paid to the other player, and portion 1-tau to the bank. While finite-duration (reachability) taxman games have been studied before, we present, for the first time, results on infinite-duration taxman games. It was previously shown that both Richman and poorman infinite-duration games with qualitative objectives reduce to reachability games, and we show a similar result here. Our most interesting results concern quantitative taxman games, namely mean-payoff games, where poorman and Richman bidding differ significantly. A central quantity in these games is the ratio between the two players' initial budgets. While in poorman mean-payoff games, the optimal payoff of a player depends on the initial ratio, in Richman bidding, the payoff depends only on the structure of the game. In both games the optimal payoffs can be found using (different) probabilistic connections with random-turn games in which in each turn, instead of bidding, a coin is tossed to determine which player moves. While the value with Richman bidding equals the value of a random-turn game with an un-biased coin, with poorman bidding, the bias in the coin is the initial ratio of the budgets. We give a complete classification of mean-payoff taxman games that is based on a probabilistic connection: the value of a taxman bidding game with parameter tau and initial ratio r, equals the value of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau). Thus, we show that Richman bidding is the exception; namely, for every tau <1, the value of the game depends on the initial ratio. Our proof technique simplifies and unifies the previous proof techniques for both Richman and poorman bidding. },
author = {Avni, Guy and Henzinger, Thomas A and Zikelic, Dorde},
location = {Aachen, Germany},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Bidding mechanisms in graph games}},
doi = {10.4230/LIPICS.MFCS.2019.11},
volume = {138},
year = {2019},
}
@inproceedings{6822,
abstract = {In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the qualitative winner or quantitative payoff of the game. In bidding games, in each turn, we hold an auction between the two players to determine which player moves the token. Bidding games have largely been studied with concrete bidding mechanisms that are variants of a first-price auction: in each turn both players simultaneously submit bids, the higher
bidder moves the token, and pays his bid to the lower bidder in Richman bidding, to the bank in poorman bidding, and in taxman bidding, the bid is split between the other player and the bank according to a predefined constant factor. Bidding games are deterministic games. They have an intriguing connection with a fragment of stochastic games called
randomturn games. We study, for the first time, a combination of bidding games with probabilistic behavior; namely, we study bidding games that are played on Markov decision processes, where the players bid for the right to choose the next action, which determines the probability distribution according to which the next vertex is chosen. We study parity and meanpayoff bidding games on MDPs and extend results from the deterministic bidding setting to the probabilistic one.},
author = {Avni, Guy and Henzinger, Thomas A and Ibsen-Jensen, Rasmus and Novotny, Petr},
booktitle = { Proceedings of the 13th International Conference of Reachability Problems},
isbn = {978-303030805-6},
issn = {0302-9743},
location = {Brussels, Belgium},
pages = {1--12},
publisher = {Springer},
title = {{Bidding games on Markov decision processes}},
doi = {10.1007/978-3-030-30806-3_1},
volume = {11674},
year = {2019},
}
@inproceedings{6985,
abstract = {In this paper, we introduce a novel method to interpret recurrent neural networks (RNNs), particularly long short-term memory networks (LSTMs) at the cellular level. We propose a systematic pipeline for interpreting individual hidden state dynamics within the network using response characterization methods. The ranked contribution of individual cells to the network's output is computed by analyzing a set of interpretable metrics of their decoupled step and sinusoidal responses. As a result, our method is able to uniquely identify neurons with insightful dynamics, quantify relationships between dynamical properties and test accuracy through ablation analysis, and interpret the impact of network capacity on a network's dynamical distribution. Finally, we demonstrate the generalizability and scalability of our method by evaluating a series of different benchmark sequential datasets.},
author = {Hasani, Ramin and Amini, Alexander and Lechner, Mathias and Naser, Felix and Grosu, Radu and Rus, Daniela},
booktitle = {Proceedings of the International Joint Conference on Neural Networks},
isbn = {9781728119854},
location = {Budapest, Hungary},
publisher = {IEEE},
title = {{Response characterization for auditing cell dynamics in long short-term memory networks}},
doi = {10.1109/ijcnn.2019.8851954},
year = {2019},
}
@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{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{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{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{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},
}
@article{6761,
abstract = {In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability.},
author = {Avni, Guy and Henzinger, Thomas A and Kupferman, Orna},
issn = {03043975},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
title = {{Dynamic resource allocation games}},
doi = {10.1016/j.tcs.2019.06.031},
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},
}
@inproceedings{5959,
abstract = {Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain.},
author = {Bakhirkin, Alexey and Ferrere, Thomas and Henzinger, Thomas A and Nickovicl, Deian},
booktitle = {2018 International Conference on Embedded Software (EMSOFT)},
isbn = {9781538655603},
location = {Turin, Italy},
pages = {1--10},
publisher = {IEEE},
title = {{Keynote: The first-order logic of signals}},
doi = {10.1109/emsoft.2018.8537203},
year = {2018},
}
@inproceedings{78,
abstract = {We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal ω that match a given temporal pattern ϕ. As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by ϕ and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads ω, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated.},
author = {Bakhirkin, Alexey and Ferrere, Thomas and Nickovic, Dejan and Maler, Oded and Asarin, Eugene},
isbn = {978-3-030-00150-6},
location = {Bejing, China},
pages = {215 -- 232},
publisher = {Springer},
title = {{Online timed pattern matching using automata}},
doi = {10.1007/978-3-030-00151-3_13},
volume = {11022},
year = {2018},
}