-
Designing an Objective-Driven Test Method for the Comparative Performance Evaluation of Commercial DTI Solutions for Counter UAS systems
Authors:
Ali Mohamoud,
Johan van de Pol,
Hanno Hildmann,
Rob van Heijster,
Beatrice Masini,
Martijn van den Heuvel,
Amber van Keeken
Abstract:
Unmanned Aerial Systems (UASs) or drones become more and more commercially available and cheap. There has been much emphasis on develo** and deploying Counter-UAS systems (UASs) with Detection Tracking and Identification (DTI) solutions. However, the capabilities of these systems are hard to benchmark. Performance claims of these systems are currently not supported by evidence. In addition, no s…
▽ More
Unmanned Aerial Systems (UASs) or drones become more and more commercially available and cheap. There has been much emphasis on develo** and deploying Counter-UAS systems (UASs) with Detection Tracking and Identification (DTI) solutions. However, the capabilities of these systems are hard to benchmark. Performance claims of these systems are currently not supported by evidence. In addition, no standard test methodologies are available for these DTI systems and different test methodologies make comparison of these systems hard or impossible. We report on the definition, development and verification of an objective-driven test method and corresponding comparative performance evaluation for commercial DTI solutions for C-UASs. The developed methodology is based on end-user scenarios that are operationally relevant. The test methodology is based on a generic DTI system lay-out and is detailed towards detection, tracking and identification, taking into account contextual information and end-user input. The comparative performance evaluation is developed to enable the use of the methodology in a relevant environment, thereby taking into account any potential environmental aspect that might influence DTI system performance. Validation of the work in a relevant environment has been done in three operational trials. The operational trial results show that the method allows for performance evaluation at component level (i.e., detection, tracking or identification component) and at system level (combinations of these components and integrated DTI system of system solutions).
△ Less
Submitted 5 June, 2024; v1 submitted 7 May, 2024;
originally announced May 2024.
-
Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
Authors:
Irfansha Shaik,
Jaco van de Pol
Abstract:
Layout synthesis is map** a quantum circuit to a quantum processor. SWAP gate insertions are needed for scheduling 2-qubit gates only on connected physical qubits. With the ever-increasing number of qubits in NISQ processors, scalable layout synthesis is of utmost importance. With large optimality gaps observed in heuristic approaches, scalable exact methods are needed. While recent exact and ne…
▽ More
Layout synthesis is map** a quantum circuit to a quantum processor. SWAP gate insertions are needed for scheduling 2-qubit gates only on connected physical qubits. With the ever-increasing number of qubits in NISQ processors, scalable layout synthesis is of utmost importance. With large optimality gaps observed in heuristic approaches, scalable exact methods are needed. While recent exact and near-optimal approaches scale to moderate circuits, large deep circuits are still out of scope.
In this work, we propose a SAT encoding based on parallel plans that apply 1 SWAP and a group of CNOTs at each time step. Using domain-specific information, we maintain optimality in parallel plans while scaling to large and deep circuits. From our results, we show the scalability of our approach which significantly outperforms leading exact and near-optimal approaches (up to 100x). For the first time, we can optimally map several 8, 14, and 16 qubit circuits onto 54, 80, and 127 qubit platforms with up to 17 SWAPs. While adding optimal SWAPs, we also report near-optimal depth in our mapped circuits.
△ Less
Submitted 18 March, 2024;
originally announced March 2024.
-
On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)
Authors:
Mikael Bisgaard Dahlsen-Jensen,
Baptiste Fievet,
Laure Petrucci,
Jaco van de Pol
Abstract:
Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environmeand depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for…
▽ More
Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environmeand depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations ``in the limit''.
△ Less
Submitted 20 January, 2024;
originally announced January 2024.
-
Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Extended Paper)
Authors:
Steffan Christ Sølvsten,
Jaco van de Pol
Abstract:
The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized BDDs. This is mostly due to initializing expensive external memory data structures, even if their contents can fit entirely inside internal memory.
The contents of these auxiliary data structures always correspond to a…
▽ More
The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized BDDs. This is mostly due to initializing expensive external memory data structures, even if their contents can fit entirely inside internal memory.
The contents of these auxiliary data structures always correspond to a graph cut in an input or output BDD. Specifically, these cuts respect the levels of the BDD. We formalise the shape of these cuts and prove sound upper bounds on their maximum size for each BDD operation.
We have implemented these upper bounds within Adiar. With these bounds, it can predict whether a faster internal memory variant of the auxiliary data structures can be used. In practice, this improves Adiar's running time across the board. Specifically for the moderate-sized BDDs, this results in an average reduction of the computation time by 86.1% (median of 89.7%). In some cases, the difference is even 99.9\%. When checking equivalence of hardware circuits from the EPFL Benchmark Suite, for one of the instances the time was decreased by 52 hours.
△ Less
Submitted 10 July, 2023;
originally announced July 2023.
-
Optimal Layout Synthesis for Quantum Circuits as Classical Planning (full version)
Authors:
Irfansha Shaik,
Jaco van de Pol
Abstract:
In Layout Synthesis, the logical qubits of a quantum circuit are mapped to the physical qubits of a given quantum hardware platform, taking into account the connectivity of physical qubits. This involves inserting SWAP gates before an operation is applied on distant qubits. Optimal Layout Synthesis is crucial for practical Quantum Computing on current error-prone hardware: Minimizing the number of…
▽ More
In Layout Synthesis, the logical qubits of a quantum circuit are mapped to the physical qubits of a given quantum hardware platform, taking into account the connectivity of physical qubits. This involves inserting SWAP gates before an operation is applied on distant qubits. Optimal Layout Synthesis is crucial for practical Quantum Computing on current error-prone hardware: Minimizing the number of SWAP gates directly mitigates the error rates when running quantum circuits. In recent years, several approaches have been proposed for minimizing the required SWAP insertions. The proposed exact approaches can only scale to a small number of qubits. Proving that a number of swap insertions is optimal is much harder than producing near optimal map**s. In this paper, we provide two encodings for Optimal Layout Synthesis as a classical planning problem. We use optimal classical planners to synthesize the optimal layout for a standard set of benchmarks. Our results show the scalability of our approach compared to previous leading approaches. We can optimally map circuits with 9 qubits onto a 14 qubit platform, which could not be handled before by exact methods.
△ Less
Submitted 28 September, 2023; v1 submitted 24 April, 2023;
originally announced April 2023.
-
Search-Space Pruning with Int-Splits for Faster QBF Solving
Authors:
Maximilian Heisinger,
Irfansha Shaik,
Martina Seidl,
Jaco van de Pol
Abstract:
In many QBF encodings, sequences of Boolean variables stand for binary representations of integer variables. Examples are state labels in bounded model checking or actions in planning problems. Often not the full possible range is used, e.g., for representing six different states, three Boolean variables are required, rendering two of the eight possible assignments irrelevant for the solution of t…
▽ More
In many QBF encodings, sequences of Boolean variables stand for binary representations of integer variables. Examples are state labels in bounded model checking or actions in planning problems. Often not the full possible range is used, e.g., for representing six different states, three Boolean variables are required, rendering two of the eight possible assignments irrelevant for the solution of the problem. As QBF solvers do not have any domain-specific knowledge on the formula they process, they are not able to detect this pruning opportunity.
In this paper, we introduce the idea of int-splits, which provide domain-specific information on integer variables to QBF solvers. This is particularly appealing for parallel Divide-and-Conquer solving which partitions the search space into independently solvable sub-problems. Using this technique, we reduce the number of generated sub-problems from a full expansion to only the required subset. We then evaluate how many resources int-splits save in problems already well suited for D&C. In that context, we provide a reference implementation that splits QBF formulas into many sub-problems with or without int-splits and merges results. We finally propose a comment-based optional syntax extension to (Q)DIMACS that includes int-splits and is suited for supplying proposed guiding paths natively to D&C solvers.
△ Less
Submitted 17 April, 2023;
originally announced April 2023.
-
Operations on Fixpoint Equation Systems
Authors:
Thomas Neele,
Jaco van de Pol
Abstract:
We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swap** the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extre…
▽ More
We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swap** the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices.
△ Less
Submitted 14 May, 2024; v1 submitted 14 April, 2023;
originally announced April 2023.
-
Concise QBF Encodings for Games on a Grid (extended version)
Authors:
Irfansha Shaik,
Jaco van de Pol
Abstract:
Encoding 2-player games in QBF correctly and efficiently is challenging and error-prone. To enable concise specifications and uniform encodings of games played on grid boards, like Tic-Tac-Toe, Connect-4, Domineering, Pursuer-Evader and Breakthrough, we introduce Board-game Domain Definition Language (BDDL), inspired by the success of PDDL in the planning domain.
We provide an efficient translat…
▽ More
Encoding 2-player games in QBF correctly and efficiently is challenging and error-prone. To enable concise specifications and uniform encodings of games played on grid boards, like Tic-Tac-Toe, Connect-4, Domineering, Pursuer-Evader and Breakthrough, we introduce Board-game Domain Definition Language (BDDL), inspired by the success of PDDL in the planning domain.
We provide an efficient translation from BDDL into QBF, encoding the existence of a winning strategy of bounded depth. Our lifted encoding treats board positions symbolically and allows concise definitions of conditions, effects and winning configurations, relative to symbolic board positions. The size of the encoding grows linearly in the input model and the considered depth.
To show the feasibility of such a generic approach, we use QBF solvers to compute the critical depths of winning strategies for instances of several known games. For several games, our work provides the first QBF encoding. Unlike plan validation in SAT-based planning, validating QBF-based winning strategies is difficult. We show how to validate winning strategies using QBF certificates and interactive game play.
△ Less
Submitted 29 March, 2023;
originally announced March 2023.
-
Implicit State and Goals in QBF Encodings for Positional Games (extended version)
Authors:
Irfansha Shaik,
Valentin Mayer-Eichberger,
Jaco van de Pol,
Abdallah Saffidine
Abstract:
We address two bottlenecks for concise QBF encodings of maker-breaker positional games, like Hex and Tic-Tac-Toe. Our baseline is a QBF encoding with explicit variables for board positions and an explicit representation of winning configurations. The first improvement is inspired by lifted planning and avoids variables for explicit board positions, introducing a universal quantifier representing a…
▽ More
We address two bottlenecks for concise QBF encodings of maker-breaker positional games, like Hex and Tic-Tac-Toe. Our baseline is a QBF encoding with explicit variables for board positions and an explicit representation of winning configurations. The first improvement is inspired by lifted planning and avoids variables for explicit board positions, introducing a universal quantifier representing a symbolic board state. The second improvement represents the winning configurations implicitly, exploiting their structure. The paper evaluates the size of several encodings, depending on board size and game depth. It also reports the performance of QBF solvers on these encodings. We evaluate the techniques on Hex instances and also apply them to Harary's Tic-Tac-Toe. In particular, we study scalability to 19$\times$19 boards, played in human Hex tournaments.
△ Less
Submitted 18 January, 2023;
originally announced January 2023.
-
Efficient Convex Zone Merging in Parametric Timed Automata
Authors:
Étienne André,
Dylan Marinho,
Laure Petrucci,
Jaco van de Pol
Abstract:
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while pres…
▽ More
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.
△ Less
Submitted 9 December, 2022;
originally announced December 2022.
-
A Manifesto for Applicable Formal Methods
Authors:
Mario Gleirscher,
Jaco van de Pol,
Jim Woodcock
Abstract:
Formal methods were frequently shown to be effective and, perhaps because of that, practitioners are interested in using them more often. Still, these methods are far less applied than expected, particularly, in critical domains where they are strongly recommended and where they have the greatest potential. Our hypothesis is that formal methods still seem not to be applicable enough or ready for t…
▽ More
Formal methods were frequently shown to be effective and, perhaps because of that, practitioners are interested in using them more often. Still, these methods are far less applied than expected, particularly, in critical domains where they are strongly recommended and where they have the greatest potential. Our hypothesis is that formal methods still seem not to be applicable enough or ready for their intended use. In critical software engineering, what do we mean when we speak of a formal method? And what does it mean for such a method to be applicable both from a scientific and practical viewpoint? Based on what the literature tells about the first question, with this manifesto, we lay out a set of principles that when followed by a formal method give rise to its mature applicability in a given scope. Rather than exercising criticism of past developments, this manifesto strives to foster an increased use of formal methods to the maximum benefit.
△ Less
Submitted 22 August, 2023; v1 submitted 23 December, 2021;
originally announced December 2021.
-
Proceedings First Workshop on Applicable Formal Methods
Authors:
Mario Gleirscher,
Jaco van de Pol,
Jim Woodcock
Abstract:
This volume contains the proceedings of the 1st International Workshop on Applicable Formal Methods (AppFM 2021), 23 November 2021, held online as part of the 24th International Symposium on Formal Methods (FM). The aim of the AppFM workshop is to bring together researchers who improve and evaluate existing formal approaches and new variants in practical contexts and support the transfer of these…
▽ More
This volume contains the proceedings of the 1st International Workshop on Applicable Formal Methods (AppFM 2021), 23 November 2021, held online as part of the 24th International Symposium on Formal Methods (FM). The aim of the AppFM workshop is to bring together researchers who improve and evaluate existing formal approaches and new variants in practical contexts and support the transfer of these approaches to software engineering practice.
△ Less
Submitted 15 November, 2021;
originally announced November 2021.
-
A Benchmarks Library for Extended Parametric Timed Automata
Authors:
Étienne André,
Dylan Marinho,
Jaco van de Pol
Abstract:
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new algorithms, a fair set of benchmarks is required. We present an extension of the IMITATOR benchmarks library, that accumulated over the years a number of case studies from academic and industrial contexts. We extend here…
▽ More
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new algorithms, a fair set of benchmarks is required. We present an extension of the IMITATOR benchmarks library, that accumulated over the years a number of case studies from academic and industrial contexts. We extend here the library with several dozens of new benchmarks; these benchmarks highlight several new features: liveness properties, extensions of (parametric) timed automata (including stopwatches or multi-rate clocks), and unsolvable toy benchmarks. These latter additions help to emphasize the limits of state-of-the-art parameter synthesis techniques, with the hope to develop new dedicated algorithms in the future.
△ Less
Submitted 18 June, 2021;
originally announced June 2021.
-
Classical Planning as QBF without Grounding (extended version)
Authors:
Irfansha Shaik,
Jaco van de Pol
Abstract:
Most classical planners use grounding as a preprocessing step, essentially reducing planning to propositional logic. However, grounding involves instantiating all action rules with concrete object combinations, and results in large encodings for SAT/QBF-based planners. This severe cost in memory becomes a main bottleneck when actions have many parameters, such as in the Organic Synthesis problems…
▽ More
Most classical planners use grounding as a preprocessing step, essentially reducing planning to propositional logic. However, grounding involves instantiating all action rules with concrete object combinations, and results in large encodings for SAT/QBF-based planners. This severe cost in memory becomes a main bottleneck when actions have many parameters, such as in the Organic Synthesis problems from the IPC 2018 competition. We provide a compact QBF encoding that is logarithmic in the number of objects and avoids grounding completely, by using universal quantification for object combinations. We show that we can solve some of the Organic Synthesis problems, which could not be handled before by any SAT/QBF based planners due to grounding.
△ Less
Submitted 18 December, 2021; v1 submitted 18 June, 2021;
originally announced June 2021.
-
Efficient Binary Decision Diagram Manipulation in External Memory
Authors:
Steffan Christ Sølvsten,
Jaco van de Pol,
Anna Blume Jakobsen,
Mathias Weller Berg Thomasen
Abstract:
We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide a…
▽ More
We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to simplify and improve the performance of his proposed algorithms. Furthermore, we extend the technique to other common BDD operations, many of which are not derivable using Apply operations alone, and we provide asymptotic improvements for the procedures that can be derived using Apply.
These algorithms are implemented in a new BDD package, named Adiar. We see very promising results when comparing the performance of Adiar with conventional BDD packages that use recursive depth-first algorithms. For instances larger than 8.2 GiB, our algorithms, in parts using the disk, are 1.47 to 3.69 times slower compared to CUDD and Sylvan, exclusively using main memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the main memory needed by conventional BDD packages to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of other BDD packages.
△ Less
Submitted 4 January, 2023; v1 submitted 25 April, 2021;
originally announced April 2021.
-
Certifying Emptiness of Timed Büchi Automata
Authors:
Simon Wimmer,
Frédéric Herbreteau,
Jaco van de Pol
Abstract:
Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at further increasing the trust in their verification results, in particular for checking liveness properties. To this end, we develop an approach for extracting certificates for the emptiness of timed Büchi automata from model…
▽ More
Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at further increasing the trust in their verification results, in particular for checking liveness properties. To this end, we develop an approach for extracting certificates for the emptiness of timed Büchi automata from model checking runs. These certificates can be double-checked by a certifier that we formally verify in Isabelle/HOL. We study liveness certificates in an abstract setting and show that our approach is sound and complete. To also demonstrate its feasibility, we extract certificates for several models checked by TChecker and Imitator, and validate them with our verified certifier.
△ Less
Submitted 8 July, 2020;
originally announced July 2020.
-
Minimal-Time Synthesis for Parametric Timed Automata
Authors:
Étienne André,
Vincent Bloemen,
Laure Petrucci,
Jaco van de Pol
Abstract:
Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks.
We focu…
▽ More
Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks.
We focus on synthesizing parameters such that not only the goal location is reached, but we also address the following questions: what is the minimal time to reach the goal location? and for which parameter values can we achieve this? We analyse the problem and present an algorithm that solves it. We also discuss and provide solutions for minimizing a specific parameter value to still reach the goal.
We empirically study the performance of these algorithms on a benchmark set for PTAs and show that minimal-time reachability synthesis is more efficient to compute than the standard synthesis algorithm for reachability.
△ Less
Submitted 8 February, 2019;
originally announced February 2019.
-
Symbolic Reachability Analysis of B through ProB and LTSmin
Authors:
Jens Bendisposto,
Philipp Koerner,
Michael Leuschel,
Jeroen Meijer,
Jaco van de Pol,
Helen Treharne,
Jorden Whitefield
Abstract:
We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few…
▽ More
We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few hundred lines of glue-code, along with a bridge between ProB and C using ZeroMQ. ProB supports model checking of several formal specification languages such as B, Event-B, Z and TLA. Our experiments are based on a wide variety of B-Method and Event-B models to demonstrate the efficiency of the new link. Among the tested categories are state space generation and deadlock detection; but action detection and invariant checking are also feasible in principle. In many cases we observe speedups of several orders of magnitude. We also compare the results with other approaches for improving model checking, such as partial order reduction or symmetry reduction. We thus provide a new scalable, symbolic analysis algorithm for the B-Method and Event-B, along with a platform to integrate other model checking improvements via LTSmin in the future.
△ Less
Submitted 14 March, 2016;
originally announced March 2016.
-
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Model Checking
Authors:
Jeroen Meijer,
Jaco van de Pol
Abstract:
We demonstrate the applicability of bandwidth and wavefront reduction algorithms to static variable ordering. In symbolic model checking event locality plays a major role in time and memory usage. For example, in Petri nets event locality can be captured by dependency matrices, where nonzero entries indicate whether a transition modifies a place. The quality of event locality has been expressed as…
▽ More
We demonstrate the applicability of bandwidth and wavefront reduction algorithms to static variable ordering. In symbolic model checking event locality plays a major role in time and memory usage. For example, in Petri nets event locality can be captured by dependency matrices, where nonzero entries indicate whether a transition modifies a place. The quality of event locality has been expressed as a metric called (weighted) event span. The bandwidth of a matrix is a metric indicating the distance of nonzero elements to the diagonal. Wavefront is a metric indicating the degree of nonzeros on one end of the diagonal of the matrix. Bandwidth and wavefront are well studied metrics used in sparse matrix solvers.
In this work we prove that span is limited by twice the bandwidth of a matrix. This observation makes bandwidth reduction algorithms useful for obtaining good variable orders. One major issue we address is that the reduction algorithms can only be applied on symmetric matrices, while the dependency matrices are asymmetric. We show that the Sloan algorithm executed on the total graph of the adjacency graph gives the best variable orders. Practically, we demonstrate that our work allows to call standard sparse matrix operations in Boost and ViennaCL, computing very good static variable orders in milliseconds. Future work is promising, because a whole new spectrum of more off-the-shelf algorithms, including metaheuristic ones, become available for variable ordering.
△ Less
Submitted 27 November, 2015;
originally announced November 2015.
-
Modeling and Verification of the Bitcoin Protocol
Authors:
Kaylash Chaudhary,
Ansgar Fehnker,
Jaco van de Pol,
Marielle Stoelinga
Abstract:
Bitcoin is a popular digital currency for online payments, realized as a decentralized peer-to-peer electronic cash system. Bitcoin keeps a ledger of all transactions; the majority of the participants decides on the correct ledger. Since there is no trusted third party to guard against double spending, and inspired by its popularity, we would like to investigate the correctness of the Bitcoin prot…
▽ More
Bitcoin is a popular digital currency for online payments, realized as a decentralized peer-to-peer electronic cash system. Bitcoin keeps a ledger of all transactions; the majority of the participants decides on the correct ledger. Since there is no trusted third party to guard against double spending, and inspired by its popularity, we would like to investigate the correctness of the Bitcoin protocol. Double spending is an important threat to electronic payment systems. Double spending would happen if one user could force a majority to believe that a ledger without his previous payment is the correct one. We are interested in the probability of success of such a double spending attack, which is linked to the computational power of the attacker. This paper examines the Bitcoin protocol and provides its formalization as an UPPAAL model. The model will be used to show how double spending can be done if the parties in the Bitcoin protocol behave maliciously, and with what probability double spending occurs.
△ Less
Submitted 13 November, 2015;
originally announced November 2015.
-
Generating and Solving Symbolic Parity Games
Authors:
Gijs Kant,
Jaco van de Pol
Abstract:
We present a new tool for verification of modal mu-calculus formulae for process specifications, based on symbolic parity games. It enhances an existing method, that first encodes the problem to a Parameterised Boolean Equation System (PBES) and then instantiates the PBES to a parity game. We improved the translation from specification to PBES to preserve the structure of the specification in the…
▽ More
We present a new tool for verification of modal mu-calculus formulae for process specifications, based on symbolic parity games. It enhances an existing method, that first encodes the problem to a Parameterised Boolean Equation System (PBES) and then instantiates the PBES to a parity game. We improved the translation from specification to PBES to preserve the structure of the specification in the PBES, we extended LTSmin to instantiate PBESs to symbolic parity games, and implemented the recursive parity game solving algorithm by Zielonka for symbolic parity games. We use Multi-valued Decision Diagrams (MDDs) to represent sets and relations, thus enabling the tools to deal with very large systems. The transition relation is partitioned based on the structure of the specification, which allows for efficient manipulation of the MDDs. We performed two case studies on modular specifications, that demonstrate that the new method has better time and memory performance than existing PBES based tools and can be faster (but slightly less memory efficient) than the symbolic model checker NuSMV.
△ Less
Submitted 29 July, 2014;
originally announced July 2014.
-
Setting Parameters for Biological Models With ANIMO
Authors:
Stefano Schivo,
Jetse Scholma,
Marcel Karperien,
Janine N. Post,
Jaco van de Pol,
Rom Langerak
Abstract:
ANIMO (Analysis of Networks with Interactive MOdeling) is a software for modeling biological networks, such as e.g. signaling, metabolic or gene networks. An ANIMO model is essentially the sum of a network topology and a number of interaction parameters. The topology describes the interactions between biological entities in form of a graph, while the parameters determine the speed of occurrence of…
▽ More
ANIMO (Analysis of Networks with Interactive MOdeling) is a software for modeling biological networks, such as e.g. signaling, metabolic or gene networks. An ANIMO model is essentially the sum of a network topology and a number of interaction parameters. The topology describes the interactions between biological entities in form of a graph, while the parameters determine the speed of occurrence of such interactions. When a mismatch is observed between the behavior of an ANIMO model and experimental data, we want to update the model so that it explains the new data. In general, the topology of a model can be expanded with new (known or hypothetical) nodes, and enables it to match experimental data. However, the unrestrained addition of new parts to a model causes two problems: models can become too complex too fast, to the point of being intractable, and too many parts marked as "hypothetical" or "not known" make a model unrealistic. Even if changing the topology is normally the easier task, these problems push us to try a better parameter fit as a first step, and resort to modifying the model topology only as a last resource. In this paper we show the support added in ANIMO to ease the task of expanding the knowledge on biological networks, concentrating in particular on the parameter settings.
△ Less
Submitted 1 April, 2014;
originally announced April 2014.
-
Solving the Shortest Vector Problem in Lattices Faster Using Quantum Search
Authors:
Thijs Laarhoven,
Michele Mosca,
Joop van de Pol
Abstract:
By applying Grover's quantum search algorithm to the lattice algorithms of Micciancio and Voulgaris, Nguyen and Vidick, Wang et al., and Pujol and Stehlé, we obtain improved asymptotic quantum results for solving the shortest vector problem. With quantum computers we can provably find a shortest vector in time $2^{1.799n + o(n)}$, improving upon the classical time complexity of…
▽ More
By applying Grover's quantum search algorithm to the lattice algorithms of Micciancio and Voulgaris, Nguyen and Vidick, Wang et al., and Pujol and Stehlé, we obtain improved asymptotic quantum results for solving the shortest vector problem. With quantum computers we can provably find a shortest vector in time $2^{1.799n + o(n)}$, improving upon the classical time complexity of $2^{2.465n + o(n)}$ of Pujol and Stehlé and the $2^{2n + o(n)}$ of Micciancio and Voulgaris, while heuristically we expect to find a shortest vector in time $2^{0.312n + o(n)}$, improving upon the classical time complexity of $2^{0.384n + o(n)}$ of Wang et al. These quantum complexities will be an important guide for the selection of parameters for post-quantum cryptosystems based on the hardness of the shortest vector problem.
△ Less
Submitted 25 January, 2013;
originally announced January 2013.
-
Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games
Authors:
Gijs Kant,
Jaco van de Pol
Abstract:
Parameterised Boolean Equation Systems (PBESs) are sequences of Boolean fixed point equations with data variables, used for, e.g., verification of modal mu-calculus formulae for process algebraic specifications with data.
Solving a PBES is usually done by instantiation to a Parity Game and then solving the game. Practical game solvers exist, but the instantiation step is the bottleneck.
We enh…
▽ More
Parameterised Boolean Equation Systems (PBESs) are sequences of Boolean fixed point equations with data variables, used for, e.g., verification of modal mu-calculus formulae for process algebraic specifications with data.
Solving a PBES is usually done by instantiation to a Parity Game and then solving the game. Practical game solvers exist, but the instantiation step is the bottleneck.
We enhance the instantiation in two steps. First, we transform the PBES to a Parameterised Parity Game (PPG), a PBES with each equation either conjunctive or disjunctive. Then we use LTSmin, that offers transition caching, efficient storage of states and both distributed and symbolic state space generation, for generating the game graph. To that end we define a language module for LTSmin, consisting of an encoding of variables with parameters into state vectors, a grouped transition relation and a dependency matrix to indicate the dependencies between parts of the state vector and transition groups.
Benchmarks on some large case studies, show that the method speeds up the instantiation significantly and decreases memory usage drastically.
△ Less
Submitted 23 October, 2012;
originally announced October 2012.
-
Variations on Multi-Core Nested Depth-First Search
Authors:
Alfons Laarman,
Jaco van de Pol
Abstract:
Recently, two new parallel algorithms for on-the-fly model checking of LTL properties were presented at the same conference: Automated Technology for Verification and Analysis, 2011. Both approaches extend Swarmed NDFS, which runs several sequential NDFS instances in parallel. While parallel random search already speeds up detection of bugs, the workers must share some global information in order…
▽ More
Recently, two new parallel algorithms for on-the-fly model checking of LTL properties were presented at the same conference: Automated Technology for Verification and Analysis, 2011. Both approaches extend Swarmed NDFS, which runs several sequential NDFS instances in parallel. While parallel random search already speeds up detection of bugs, the workers must share some global information in order to speed up full verification of correct models. The two algorithms differ considerably in the global information shared between workers, and in the way they synchronize.
Here, we provide a thorough experimental comparison between the two algorithms, by measuring the runtime of their implementations on a multi-core machine. Both algorithms were implemented in the same framework of the model checker LTSmin, using similar optimizations, and have been subjected to the full BEEM model database.
Because both algorithms have complementary advantages, we constructed an algorithm that combines both ideas. This combination clearly has an improved speedup. We also compare the results with the alternative parallel algorithm for accepting cycle detection OWCTY-MAP. Finally, we study a simple statistical model for input models that do contain accepting cycles. The goal is to distinguish the speedup due to parallel random search from the speedup that can be attributed to clever work sharing schemes.
△ Less
Submitted 1 November, 2011;
originally announced November 2011.
-
Parallel Recursive State Compression for Free
Authors:
Alfons Laarman,
Jaco van de Pol,
Michael Weber
Abstract:
This paper focuses on reducing memory usage in enumerative model checking, while maintaining the multi-core scalability obtained in earlier work. We present a tree-based multi-core compression method, which works by leveraging sharing among sub-vectors of state vectors.
An algorithmic analysis of both worst-case and optimal compression ratios shows the potential to compress even large states to…
▽ More
This paper focuses on reducing memory usage in enumerative model checking, while maintaining the multi-core scalability obtained in earlier work. We present a tree-based multi-core compression method, which works by leveraging sharing among sub-vectors of state vectors.
An algorithmic analysis of both worst-case and optimal compression ratios shows the potential to compress even large states to a small constant on average (8 bytes). Our experiments demonstrate that this holds up in practice: the median compression ratio of 279 measured experiments is within 17% of the optimum for tree compression, and five times better than the median compression ratio of SPIN's COLLAPSE compression.
Our algorithms are implemented in the LTSmin tool, and our experiments show that for model checking, multi-core tree compression pays its own way: it comes virtually without overhead compared to the fastest hash table-based methods.
△ Less
Submitted 14 May, 2011; v1 submitted 15 April, 2011;
originally announced April 2011.
-
Confluence Reduction for Probabilistic Systems (extended version)
Authors:
Mark Timmer,
Mariëlle Stoelinga,
Jaco van de Pol
Abstract:
This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic pr…
▽ More
This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained.
△ Less
Submitted 10 November, 2010;
originally announced November 2010.
-
Boosting Multi-Core Reachability Performance with Shared Hash Tables
Authors:
Alfons Laarman,
Jaco van de Pol,
Michael Weber
Abstract:
This paper focuses on data structures for multi-core reachability, which is a key component in model checking algorithms and other verification methods. A cornerstone of an efficient solution is the storage of visited states. In related work, static partitioning of the state space was combined with thread-local storage and resulted in reasonable speedups, but left open whether improvements are…
▽ More
This paper focuses on data structures for multi-core reachability, which is a key component in model checking algorithms and other verification methods. A cornerstone of an efficient solution is the storage of visited states. In related work, static partitioning of the state space was combined with thread-local storage and resulted in reasonable speedups, but left open whether improvements are possible. In this paper, we present a scaling solution for shared state storage which is based on a lockless hash table implementation. The solution is specifically designed for the cache architecture of modern CPUs. Because model checking algorithms impose loose requirements on the hash table operations, their design can be streamlined substantially compared to related work on lockless hash tables. Still, an implementation of the hash table presented here has dozens of sensitive performance parameters (bucket size, cache line size, data layout, probing sequence, etc.). We analyzed their impact and compared the resulting speedups with related tools. Our implementation outperforms two state-of-the-art multi-core model checkers (SPIN and DiVinE) by a substantial margin, while placing fewer constraints on the load balancing and search algorithms.
△ Less
Submitted 4 May, 2010; v1 submitted 16 April, 2010;
originally announced April 2010.
-
Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation
Authors:
Lubos Brim,
Jaco van de Pol
Abstract:
The 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2009) took place on November 4, 2009 at the Eindhoven University of Technology, in conjunction with Formal Methods 2009 and other related events for the first time under the heading of Formal Methods Week. This volume contains the final workshop proceedings.
The 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2009) took place on November 4, 2009 at the Eindhoven University of Technology, in conjunction with Formal Methods 2009 and other related events for the first time under the heading of Formal Methods Week. This volume contains the final workshop proceedings.
△ Less
Submitted 15 December, 2009;
originally announced December 2009.
-
Distributed Branching Bisimulation Minimization by Inductive Signatures
Authors:
Stefan Blom,
Jaco van de Pol
Abstract:
We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the input graph contains no tau-loops.
The optimization in the refinement process is meant to reduce both the number of iterations needed and the memo…
▽ More
We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the input graph contains no tau-loops.
The optimization in the refinement process is meant to reduce both the number of iterations needed and the memory requirements. In the former case we cannot prove that there is an improvement, but our experiments show that in many cases the number of iterations is smaller. In the latter case, we can prove that the worst case memory use of the new algorithm is linear in the size of the state space, whereas the old algorithm has a quadratic upper bound.
The paper includes a proof of correctness of the new algorithm and the results of a number of experiments that compare the performance of the old and the new algorithms.
△ Less
Submitted 13 December, 2009;
originally announced December 2009.
