@inproceedings{8599,
abstract = {A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.},
author = {Avni, Guy and Henzinger, Thomas A},
booktitle = {31st International Conference on Concurrency Theory},
isbn = {9783959771603},
issn = {18688969},
location = {Virtual},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{A survey of bidding games on graphs}},
doi = {10.4230/LIPIcs.CONCUR.2020.2},
volume = {171},
year = {2020},
}
@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},
pages = {42--55},
publisher = {Elsevier},
title = {{Dynamic resource allocation games}},
doi = {10.1016/j.tcs.2019.06.031},
volume = {807},
year = {2020},
}
@article{7426,
abstract = {This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state–space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state–space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method.},
author = {Garcia Soto, Miriam and Prabhakar, Pavithra},
issn = {1751570X},
journal = {Nonlinear Analysis: Hybrid Systems},
number = {5},
publisher = {Elsevier},
title = {{Abstraction based verification of stability of polyhedral switched systems}},
doi = {10.1016/j.nahs.2020.100856},
volume = {36},
year = {2020},
}
@article{8679,
abstract = {A central goal of artificial intelligence in high-stakes decision-making applications is to design a single algorithm that simultaneously expresses generalizability by learning coherent representations of their world and interpretable explanations of its dynamics. Here, we combine brain-inspired neural computation principles and scalable deep learning architectures to design compact neural controllers for task-specific compartments of a full-stack autonomous vehicle control system. We discover that a single algorithm with 19 control neurons, connecting 32 encapsulated input features to outputs by 253 synapses, learns to map high-dimensional inputs into steering commands. This system shows superior generalizability, interpretability and robustness compared with orders-of-magnitude larger black-box learning systems. The obtained neural agents enable high-fidelity autonomy for task-specific parts of a complex autonomous system.},
author = {Lechner, Mathias and Hasani, Ramin and Amini, Alexander and Henzinger, Thomas A and Rus, Daniela and Grosu, Radu},
issn = {2522-5839},
journal = {Nature Machine Intelligence},
pages = {642--652},
publisher = {Springer Nature},
title = {{Neural circuit policies enabling auditable autonomy}},
doi = {10.1038/s42256-020-00237-3},
volume = {2},
year = {2020},
}
@inproceedings{8704,
abstract = {Traditional robotic control suits require profound task-specific knowledge for designing, building and testing control software. The rise of Deep Learning has enabled end-to-end solutions to be learned entirely from data, requiring minimal knowledge about the application area. We design a learning scheme to train end-to-end linear dynamical systems (LDS)s by gradient descent in imitation learning robotic domains. We introduce a new regularization loss component together with a learning algorithm that improves the stability of the learned autonomous system, by forcing the eigenvalues of the internal state updates of an LDS to be negative reals. We evaluate our approach on a series of real-life and simulated robotic experiments, in comparison to linear and nonlinear Recurrent Neural Network (RNN) architectures. Our results show that our stabilizing method significantly improves test performance of LDS, enabling such linear models to match the performance of contemporary nonlinear RNN architectures. A video of the obstacle avoidance performance of our method on a mobile robot, in unseen environments, compared to other methods can be viewed at https://youtu.be/mhEsCoNao5E.},
author = {Lechner, Mathias and Hasani, Ramin and Rus, Daniela and Grosu, Radu},
booktitle = {Proceedings - IEEE International Conference on Robotics and Automation},
isbn = {9781728173955},
issn = {10504729},
location = {Paris, France},
pages = {5446--5452},
publisher = {IEEE},
title = {{Gershgorin loss stabilizes the recurrent neural network compartment of an end-to-end robot learning scheme}},
doi = {10.1109/ICRA40945.2020.9196608},
year = {2020},
}
@inproceedings{8623,
abstract = {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.},
author = {Henzinger, Thomas A and Sarac, Naci E},
booktitle = {Runtime Verification},
isbn = {9783030605070},
issn = {0302-9743},
location = {Los Angeles, CA, United States},
pages = {3--18},
publisher = {Springer Nature},
title = {{Monitorability under assumptions}},
doi = {10.1007/978-3-030-60508-7_1},
volume = {12399},
year = {2020},
}
@unpublished{8750,
abstract = {Efficiently handling time-triggered and possibly nondeterministic switches
for hybrid systems reachability is a challenging task. In this paper we present
an approach based on conservative set-based enclosure of the dynamics that can
handle systems with uncertain parameters and inputs, where the uncertainties
are bound to given intervals. The method is evaluated on the plant model of an
experimental electro-mechanical braking system with periodic controller. In
this model, the fast-switching controller dynamics requires simulation time
scales of the order of nanoseconds. Accurate set-based computations for
relatively large time horizons are known to be expensive. However, by
appropriately decoupling the time variable with respect to the spatial
variables, and enclosing the uncertain parameters using interval matrix maps
acting on zonotopes, we show that the computation time can be lowered to 5000
times faster with respect to previous works. This is a step forward in formal
verification of hybrid systems because reduced run-times allow engineers to
introduce more expressiveness in their models with a relatively inexpensive
computational cost.},
author = {Forets, Marcelo and Freire, Daniel and Schilling, Christian},
booktitle = {arXiv},
title = {{Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions}},
year = {2020},
}
@inproceedings{8287,
abstract = {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 paper, 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.},
author = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
booktitle = {Proceedings of the International Conference on Embedded Software},
keywords = {Reachability, Hybrid systems, Decomposition},
location = {Virtual },
title = {{Reachability analysis of linear hybrid systems via block decomposition}},
year = {2020},
}
@article{8790,
abstract = {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.},
author = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
issn = {19374151},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
number = {11},
pages = {4018--4029},
publisher = {IEEE},
title = {{Reachability analysis of linear hybrid systems via block decomposition}},
doi = {10.1109/TCAD.2020.3012859},
volume = {39},
year = {2020},
}
@inproceedings{7147,
abstract = {The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets.
In this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest.
The behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions.},
author = {Guet, Calin C and Henzinger, Thomas A and Igler, Claudia and Petrov, Tatjana and Sezgin, Ali},
booktitle = {17th International Conference on Computational Methods in Systems Biology},
isbn = {9783030313036},
issn = {1611-3349},
location = {Trieste, Italy},
pages = {155--187},
publisher = {Springer Nature},
title = {{Transient memory in gene regulation}},
doi = {10.1007/978-3-030-31304-3_9},
volume = {11773},
year = {2019},
}