@inproceedings{9202,
abstract = {We propose a novel hybridization method for stability analysis that over-approximates nonlinear dynamical systems by switched systems with linear inclusion dynamics. We observe that existing hybridization techniques for safety analysis that over-approximate nonlinear dynamical systems by switched affine inclusion dynamics and provide fixed approximation error, do not suffice for stability analysis. Hence, we propose a hybridization method that provides a state-dependent error which converges to zero as the state tends to the equilibrium point. The crux of our hybridization computation is an elegant recursive algorithm that uses partial derivatives of a given function to obtain upper and lower bound matrices for the over-approximating linear inclusion. We illustrate our method on some examples to demonstrate the application of the theory for stability analysis. In particular, our method is able to establish stability of a nonlinear system which does not admit a polynomial Lyapunov function.},
author = {Garcia Soto, Miriam and Prabhakar, Pavithra},
booktitle = {2020 IEEE Real-Time Systems Symposium},
issn = {2576-3172},
location = {Houston, TX, USA },
pages = {244--256},
publisher = {IEEE},
title = {{Hybridization for stability verification of nonlinear switched systems}},
doi = {10.1109/RTSS49844.2020.00031},
year = {2021},
}
@article{9239,
abstract = {A graph game proceeds as follows: two players move a token through a graph to produce a finite or infinite path, which determines the payoff of the game. We study bidding games in which in each turn, an auction determines which player moves the token. Bidding games were largely studied in combination with two variants of first-price auctions called “Richman” and “poorman” bidding. We study taxman bidding, which span the spectrum between the two. The game is parameterized by a constant : portion τ of the winning bid is paid to the other player, and portion 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: we unify, generalize, and simplify previous equivalences between bidding games and a class of stochastic games called random-turn games.},
author = {Avni, Guy and Henzinger, Thomas A and Žikelić, Đorđe},
issn = {1090-2724},
journal = {Journal of Computer and System Sciences},
number = {8},
pages = {133--144},
publisher = {Elsevier},
title = {{Bidding mechanisms in graph games}},
doi = {10.1016/j.jcss.2021.02.008},
volume = {119},
year = {2021},
}
@article{8912,
abstract = {For automata, synchronization, the problem of bringing an automaton to a particular state regardless of its initial state, is important. It has several applications in practice and is related to a fifty-year-old conjecture on the length of the shortest synchronizing word. Although using shorter words increases the effectiveness in practice, finding a shortest one (which is not necessarily unique) is NP-hard. For this reason, there exist various heuristics in the literature. However, high-quality heuristics such as SynchroP producing relatively shorter sequences are very expensive and can take hours when the automaton has tens of thousands of states. The SynchroP heuristic has been frequently used as a benchmark to evaluate the performance of the new heuristics. In this work, we first improve the runtime of SynchroP and its variants by using algorithmic techniques. We then focus on adapting SynchroP for many-core architectures,
and overall, we obtain more than 1000× speedup on GPUs compared to naive sequential implementation that has been frequently used as a benchmark to evaluate new heuristics in the literature. We also propose two SynchroP variants and evaluate their performance.},
author = {Sarac, Naci E and Altun, Ömer Faruk and Atam, Kamil Tolga and Karahoda, Sertac and Kaya, Kamer and Yenigün, Hüsnü},
issn = {09574174},
journal = {Expert Systems with Applications},
number = {4},
publisher = {Elsevier},
title = {{Boosting expensive synchronizing heuristics}},
doi = {10.1016/j.eswa.2020.114203},
volume = {167},
year = {2021},
}
@inproceedings{9356,
abstract = {In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a given specification. We generalize the theory of runtime verification to monitors that attempt to estimate numerical values of quantitative trace properties (instead of attempting to conclude boolean values of trace specifications), such as maximal or average response time along a trace. Quantitative monitors are approximate: with every finite prefix, they can improve their estimate of the infinite trace's unknown property value. Consequently, quantitative monitors can be compared with regard to a precision-cost trade-off: better approximations of the property value require more monitor resources, such as states (in the case of finite-state monitors) or registers, and additional resources yield better approximations. We introduce a formal framework for quantitative and approximate monitoring, show how it conservatively generalizes the classical boolean setting for monitoring, and give several precision-cost trade-offs for monitors. For example, we prove that there are quantitative properties for which every additional register improves monitoring precision.},
author = {Henzinger, Thomas A and Sarac, Naci E},
booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science},
location = {Online},
publisher = {Association for Computing Machinery},
title = {{Quantitative and approximate monitoring}},
year = {2021},
}
@article{9647,
abstract = {Gene expression is regulated by the set of transcription factors (TFs) that bind to the promoter. The ensuing regulating function is often represented as a combinational logic circuit, where output (gene expression) is determined by current input values (promoter bound TFs) only. However, the simultaneous arrival of TFs is a strong assumption, since transcription and translation of genes introduce intrinsic time delays and there is no global synchronisation among the arrival times of different molecular species at their targets. We present an experimentally implementable genetic circuit with two inputs and one output, which in the presence of small delays in input arrival, exhibits qualitatively distinct population-level phenotypes, over timescales that are longer than typical cell doubling times. From a dynamical systems point of view, these phenotypes represent long-lived transients: although they converge to the same value eventually, they do so after a very long time span. The key feature of this toy model genetic circuit is that, despite having only two inputs and one output, it is regulated by twenty-three distinct DNA-TF configurations, two of which are more stable than others (DNA looped states), one promoting and another blocking the expression of the output gene. Small delays in input arrival time result in a majority of cells in the population quickly reaching the stable state associated with the first input, while exiting of this stable state occurs at a slow timescale. In order to mechanistically model the behaviour of this genetic circuit, we used a rule-based modelling language, and implemented a grid-search to find parameter combinations giving rise to long-lived transients. Our analysis shows that in the absence of feedback, there exist path-dependent gene regulatory mechanisms based on the long timescale of transients. The behaviour of this toy model circuit suggests that gene regulatory networks can exploit event timing to create phenotypes, and it opens the possibility that they could use event timing to memorise events, without regulatory feedback. The model reveals the importance of (i) mechanistically modelling the transitions between the different DNA-TF states, and (ii) employing transient analysis thereof.},
author = {Petrov, Tatjana and Igler, Claudia and Sezgin, Ali and Henzinger, Thomas A and Guet, Calin C},
issn = {03043975},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
title = {{Long lived transients in gene regulation}},
doi = {10.1016/j.tcs.2021.05.023},
year = {2021},
}
@inproceedings{9200,
abstract = {Formal design of embedded and cyber-physical systems relies on mathematical modeling. In this paper, we consider the model class of hybrid automata whose dynamics are defined by affine differential equations. Given a set of time-series data, we present an algorithmic approach to synthesize a hybrid automaton exhibiting behavior that is close to the data, up to a specified precision, and changes in synchrony with the data. A fundamental problem in our synthesis algorithm is to check membership of a time series in a hybrid automaton. Our solution integrates reachability and optimization techniques for affine dynamical systems to obtain both a sufficient and a necessary condition for membership, combined in a refinement framework. The algorithm processes one time series at a time and hence can be interrupted, provide an intermediate result, and be resumed. We report experimental results demonstrating the applicability of our synthesis approach.},
author = {Garcia Soto, Miriam and Henzinger, Thomas A and Schilling, Christian},
booktitle = {HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control},
isbn = {9781450383394},
keywords = {hybrid automaton, membership, system identification},
location = {Nashville, TN, United States},
pages = {2102.12734},
publisher = {Association for Computing Machinery},
title = {{Synthesis of hybrid automata with affine dynamics from time-series data}},
doi = {10.1145/3447928.3456704},
year = {2021},
}
@misc{9946,
abstract = {We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.},
author = {Mühlböck, Fabian and Henzinger, Thomas A},
issn = {2664-1690},
keywords = {Run-time verification, Software engineering, Implicit specification},
pages = {17},
publisher = {IST Austria},
title = {{Differential monitoring}},
doi = {10.15479/AT:ISTA:9946},
year = {2021},
}
@unpublished{9281,
abstract = {We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's recent new proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics.},
author = {Dubach, Guillaume and Mühlböck, Fabian},
booktitle = {arXiv},
title = {{Formal verification of Zagier's one-sentence proof}},
year = {2021},
}
@inproceedings{10003,
abstract = {In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a given specification. We generalize the theory of runtime verification to monitors that attempt to estimate numerical values of quantitative trace properties (instead of attempting to conclude boolean values of trace specifications), such as maximal or average response time along a trace. Quantitative monitors are approximate: with every finite prefix, they can improve their estimate of the infinite trace's unknown property value. Consequently, quantitative monitors can be compared with regard to a precision-cost trade-off: better approximations of the property value require more monitor resources, such as states (in the case of finite-state monitors) or registers, and additional resources yield better approximations. We introduce a formal framework for quantitative and approximate monitoring, show how it conservatively generalizes the classical boolean setting for monitoring, and give several precision-cost trade-offs for monitors. For example, we prove that there are quantitative properties for which every additional register improves monitoring precision.},
author = {Henzinger, Thomas A and Sarac, Naci E},
booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science},
isbn = {978-1-6654-4896-3},
issn = {1043-6871},
keywords = {Computer science, Runtime, Registers, Time factors, Monitoring},
location = {Rome, Italy},
pages = {1--14},
publisher = {Institute of Electrical and Electronics Engineers},
title = {{Quantitative and approximate monitoring}},
doi = {10.1109/LICS52264.2021.9470547},
year = {2021},
}
@inproceedings{8012,
abstract = {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.},
author = {Kragl, Bernhard and Enea, Constantin and Henzinger, Thomas A and Mutluergil, Suha Orhun and Qadeer, Shaz},
booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
isbn = {9781450376136},
location = {London, United Kingdom},
pages = {227--242},
publisher = {Association for Computing Machinery},
title = {{Inductive sequentialization of asynchronous programs}},
doi = {10.1145/3385412.3385980},
year = {2020},
}
@inproceedings{8194,
abstract = {Fixed-point arithmetic is a popular alternative to floating-point arithmetic on embedded systems. Existing work on the verification of fixed-point programs relies on custom formalizations of fixed-point arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of fixed-point arithmetic. We present an intuitive yet comprehensive syntax of the fixed-point theory, and provide formal semantics for it based on rational arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.},
author = {Baranowski, Marek and He, Shaobo and Lechner, Mathias and Nguyen, Thanh Son and Rakamarić, Zvonimir},
booktitle = {Automated Reasoning},
isbn = {9783030510732},
issn = {16113349},
location = {Paris, France},
pages = {13--31},
publisher = {Springer Nature},
title = {{An SMT theory of fixed-point arithmetic}},
doi = {10.1007/978-3-030-51074-9_2},
volume = {12166},
year = {2020},
}
@inproceedings{8195,
abstract = {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.},
author = {Kragl, Bernhard and Qadeer, Shaz and Henzinger, Thomas A},
booktitle = {Computer Aided Verification},
isbn = {9783030532871},
issn = {0302-9743},
pages = {275--298},
publisher = {Springer Nature},
title = {{Refinement for structured concurrent programs}},
doi = {10.1007/978-3-030-53288-8_14},
volume = {12224},
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},
}
@phdthesis{8332,
abstract = {Designing and verifying concurrent programs is a notoriously challenging, time consuming, and error prone task, even for experts. This is due to the sheer number of possible interleavings of a concurrent program, all of which have to be tracked and accounted for in a formal proof. Inventing an inductive invariant that captures all interleavings of a low-level implementation is theoretically possible, but practically intractable. We develop a refinement-based verification framework that provides mechanisms to simplify proof construction by decomposing the verification task into smaller subtasks.
In a first line of work, we present a foundation for refinement reasoning over structured concurrent programs. We introduce layered concurrent programs as a compact notation to represent multi-layer refinement proofs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. Each program in this sequence is expressed as structured concurrent program, i.e., a program over (potentially recursive) procedures, imperative control flow, gated atomic actions, structured parallelism, and asynchronous concurrency. This is in contrast to existing refinement-based verifiers, which represent concurrent systems as flat transition relations. We present a powerful refinement proof rule that decomposes refinement checking over structured programs into modular verification conditions. Refinement checking is supported by a new form of modular, parameterized invariants, called yield invariants, and a linear permission system to enhance local reasoning.
In a second line of work, we present two new reduction-based program transformations that target asynchronous programs. These transformations reduce the number of interleavings that need to be considered, thus reducing the complexity of invariants. Synchronization simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Inductive sequentialization establishes sequential reductions 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.
Our approach is implemented the CIVL verifier, which has been successfully used for the verification of several complex concurrent programs. In our methodology, the overall correctness of a program is established piecemeal by focusing on the invariant required for each refinement step separately. While the programmer does the creative work of specifying the chain of programs and the inductive invariant justifying each link in the chain, the tool automatically constructs the verification conditions underlying each refinement step.},
author = {Kragl, Bernhard},
issn = {2663-337X},
pages = {120},
publisher = {IST Austria},
title = {{Verifying concurrent programs: Refinement, synchronization, sequentialization}},
doi = {10.15479/AT:ISTA:8332},
year = {2020},
}
@inproceedings{8571,
abstract = {We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.},
author = {Geretti, Luca and Alexandre Dit Sandretto, Julien and Althoff, Matthias and Benet, Luis and Chapoutot, Alexandre and Chen, Xin and Collins, Pieter and Forets, Marcelo and Freire, Daniel and Immler, Fabian and Kochdumper, Niklas and Sanders, David and Schilling, Christian},
booktitle = {EPiC Series in Computing},
pages = {49--75},
publisher = {EasyChair},
title = {{ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics}},
doi = {10.29007/zkf6},
volume = {74},
year = {2020},
}
@inproceedings{8572,
abstract = {We present the results of the ARCH 2020 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its fourth edition, eight tools have been applied to solve eight different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, C2E2, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.},
author = {Althoff, Matthias and Bak, Stanley and Bao, Zongnan and Forets, Marcelo and Frehse, Goran and Freire, Daniel and Kochdumper, Niklas and Li, Yangge and Mitra, Sayan and Ray, Rajarshi and Schilling, Christian and Schupp, Stefan and Wetzlinger, Mark},
booktitle = {EPiC Series in Computing},
pages = {16--48},
publisher = {EasyChair},
title = {{ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics}},
doi = {10.29007/7dt2},
volume = {74},
year = {2020},
}
@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},
}
@inproceedings{8600,
abstract = {A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
booktitle = {31st International Conference on Concurrency Theory},
isbn = {9783959771603},
issn = {18688969},
location = {Virtual},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Multi-dimensional long-run average problems for vector addition systems with states}},
doi = {10.4230/LIPIcs.CONCUR.2020.23},
volume = {171},
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},
}
@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},
}