| 1. |
|
|
| 2. |
- Bagheri, Maryam, et al.
(författare)
-
Magnifier : A Compositional Analysis Approach for Autonomous Traffic Control
- 2022
-
Ingår i: IEEE Transactions on Software Engineering. - 0098-5589 .- 1939-3520. ; 48:8, s. 2732-2747
-
Tidskriftsartikel (refereegranskat)abstract
- Autonomous traffic control systems are large-scale systems with critical goals. To satisfy expected properties, these systems adapt themselves to possible changes in their environment and in the system itself. The adaptation may result in further changes propagated throughout the system. For each change and its consequent adaptation, assuring the satisfaction of properties of the system at runtime is important. A prominent approach to assure the correct behavior of these systems is verification at runtime, which has strict time and memory limitations. To tackle these limitations, we propose Magnifier, an iterative, incremental, and compositional verification approach that operates on an actor-based model where actors are grouped in components, and components are augmented with a coordinator. The Magnifier idea is zooming on the area (component) affected by a change and verifying the correctness of properties of interest of the system after adapting the component to the change. Magnifier checks if the change is propagating, and if that is the case, then it zooms out to perform adaptation on a larger area to contain the change. The process is iterative and incremental, and considers areas affected by the change one by one. In Magnifier, we use the Coordinated Adaptive Actor model (CoodAA) for traffic control systems. We present a formal semantics for CoodAA as a network of Timed Input-Output Automata (TIOAs), and prove the correctness of our compositional reasoning. We implement our approach in Ptolemy II. The results of our experiments indicate that the proposed approach improves the verification time and the memory consumption compared to the non-compositional approach.
|
|
| 3. |
|
|
| 4. |
- Ben Henda, Noomene, 1978-
(författare)
-
Infinite-state Stochastic and Parameterized Systems
- 2008
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- A major current challenge consists in extending formal methods in order to handle infinite-state systems. Infiniteness stems from the fact that the system operates on unbounded data structure such as stacks, queues, clocks, integers; as well as parameterization. Systems with unbounded data structure are natural models for reasoning about communication protocols, concurrent programs, real-time systems, etc. While parameterized systems are more suitable if the system consists of an arbitrary number of identical processes which is the case for cache coherence protocols, distributed algorithms and so forth. In this thesis, we consider model checking problems for certain fundamental classes of probabilistic infinite-state systems, as well as the verification of safety properties in parameterized systems. First, we consider probabilistic systems with unbounded data structures. In particular, we study probabilistic extensions of Lossy Channel Systems (PLCS), Vector addition Systems with States (PVASS) and Noisy Turing Machine (PNTM). We show how we can describe the semantics of such models by infinite-state Markov chains; and then define certain abstract properties, which allow model checking several qualitative and quantitative problems. Then, we consider parameterized systems and provide a method which allows checking safety for several classes that differ in the topologies (linear or tree) and the semantics (atomic or non-atomic). The method is based on deriving an over-approximation which allows the use of a symbolic backward reachability scheme. For each class, the over-approximation we define guarantees monotonicity of the induced approximate transition system with respect to an appropriate order. This property is convenient in the sense that it preserves upward closedness when computing sets of predecessors.
|
|
| 5. |
- Björklund, Andreas, et al.
(författare)
-
Approximate counting of K-paths : Deterministic and in polynomial space
- 2019
-
Ingår i: 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019. - 9783959771092 ; 132
-
Konferensbidrag (refereegranskat)abstract
- A few years ago, Alon et al. [ISMB 2008] gave a simple randomized O((2e)km∊−2)-time exponential-space algorithm to approximately compute the number of paths on k vertices in a graph G up to a multiplicative error of 1 ± ∊. Shortly afterwards, Alon and Gutner [IWPEC 2009, TALG 2010] gave a deterministic exponential-space algorithm with running time (2e)k+O(log3 k)m log n whenever ∊−1 = kO(1). Recently, Brand et al. [STOC 2018] provided a speed-up at the cost of reintroducing randomization. Specifically, they gave a randomized O(4km∊−2)-time exponential-space algorithm. In this article, we revisit the algorithm by Alon and Gutner. We modify the foundation of their work, and with a novel twist, obtain the following results. We present a deterministic 4k+O(√k(log2 k+log2 ∊−1))m log n-time polynomial-space algorithm. This matches the running time of the best known deterministic polynomial-space algorithm for deciding whether a given graph G has a path on k vertices. Additionally, we present a randomized 4k+O(log k(log k+log ∊−1))m log n-time polynomial-space algorithm. While Brand et al. make non-trivial use of exterior algebra, our algorithm is very simple; we only make elementary use of the probabilistic method. Thus, the algorithm by Brand et al. runs in time 4k+o(k)m whenever ∊−1 = 2o(k), while our deterministic and randomized algorithms run in time 4k+o(k)m log n whenever ∊−1 = 2o(k 4 ) and 1 ∊−1 = 2o(log k k ), respectively. Prior to our work, no 2O(k)nO(1)-time polynomial-space algorithm was known. Additionally, our approach is embeddable in the classic framework of divide-and-color, hence it immediately extends to approximate counting of graphs of bounded treewidth; in comparison, Brand et al. note that their approach is limited to graphs of bounded pathwidth.
|
|
| 6. |
- Björklund, Andreas, et al.
(författare)
-
Computing permanents and counting Hamiltonian cycles by listing dissimilar vectors
- 2019
-
Ingår i: 46th International Colloquium on Automata, Languages, and Programming : ICALP 2019 - ICALP 2019. - 1868-8969. - 9783959771092 ; 132, s. 1-25
-
Konferensbidrag (refereegranskat)abstract
- We show that the permanent of an n × n matrix over any finite ring of r ≤ n elements can be computed with a deterministic 2n−Ω(nr ) time algorithm. This improves on a Las Vegas algorithm running in expected 2n−Ω(n/(r log r)) time, implicit in [Björklund, Husfeldt, and Lyckberg, IPL 2017]. For the permanent over the integers of a 0/1-matrix with exactly d ones per row and column, we provide a deterministic 2n−Ω(d3 n /4) time algorithm. This improves on a 2n−Ω(nd ) time algorithm in [Cygan and Pilipczuk ICALP 2013]. We also show that the number of Hamiltonian cycles in an n-vertex directed graph of average degree δ can be computed by a deterministic 2n−Ω(nδ ) time algorithm. This improves on a Las Vegas algorithm running in expected 2n−Ω(poly(n δ)) time in [Björklund, Kaski, and Koutis, ICALP 2017]. A key tool in our approach is a reduction from computing the permanent to listing pairs of dissimilar vectors from two sets of vectors, i.e., vectors over a finite set that differ in each coordinate, building on an observation of [Bax and Franklin, Algorithmica 2002]. We propose algorithms that can be used both to derandomise the construction of Bax and Franklin, and efficiently list dissimilar pairs using several algorithmic tools. We also give a simple randomised algorithm resulting in Monte Carlo algorithms within the same time bounds. Our new fast algorithms for listing dissimilar vector pairs from two sets of vectors are inspired by recent algorithms for detecting and counting orthogonal vectors by [Abboud, Williams, and Yu, SODA 2015] and [Chan and Williams, SODA 2016].
|
|
| 7. |
- Björklund, Andreas, et al.
(författare)
-
Solving systems of polynomial equations over GF(2) by a parity-counting self-reduction
- 2019
-
Ingår i: 46th International Colloquium on Automata, Languages, and Programming : ICALP 2019 - ICALP 2019. - 1868-8969. - 9783959771092 ; 132, s. 1-26
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of finding solutions to systems of polynomial equations over a finite field. Lokshtanov et al. [SODA'17] recently obtained the first worst-case algorithms that beat exhaustive search for this problem. In particular for degree-d equations modulo two in n variables, they gave an O∗2(1−1/(5d))n time algorithm, and for the special case d = 2 they gave an O∗20.876n time algorithm. We modify their approach in a way that improves these running times to O∗2(1−1/(27d))n and O∗20.804n, respectively. In particular, our latter bound - that holds for all systems of quadratic equations modulo 2 - comes close to the O∗20.792n expected time bound of an algorithm empirically found to hold for random equation systems in Bardet et al. [J. Complexity, 2013]. Our improvement involves three observations: 1. The Valiant-Vazirani lemma can be used to reduce the solution-finding problem to that of counting solutions modulo 2. 2. The monomials in the probabilistic polynomials used in this solution-counting modulo 2 have a special form that we exploit to obtain better bounds on their number than in Lokshtanov et al. [SODA'17]. 3. The problem of solution-counting modulo 2 can be “embedded” in a smaller instance of the original problem, which enables us to apply the algorithm as a subroutine to itself.
|
|
| 8. |
|
|
