1,721,213 research outputs found
Applications:Puzzles and Games
No full textMany puzzles can very naturally be described in mCRL2 and solved using the available analysis techniques such as model-checking. In this chapter, six different puzzles are specified and solved.</p
Formal Verification of an Industrial UML-like Model using mCRL2
Full text linkLow-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.</p
Reinforcement Learning with Guarantees That Hold for Ever
Full text linkReinforcement learning is a successful explore-and-exploit approach, where a controller tries to learn how to navigate an unknown environment. The principle approach is for an intelligent agent to learn how to maximise expected rewards. But what happens if the objective refers to non-terminating systems? We can obviously not wait until an infinite amount of time has passed, assess the success, and update. But what can we do? This talk will tell
Infinite choice and probability distributions an open problem: The real hotel
Full text linkWe sketch a process algebra with data and probability distributions. This allows to combine two very powerful abstraction mechanisms namely non-deterministic choice and probabilities. However, it is not clear how to define an appropriate semantics for the generalised choice over data in combination with probability density functions. The real hotel is a puzzle that exemplifies the core of the problem
Supporting Railway Innovations with Formal Modelling and Verification
Full text linkIt is a continuing challenge for European railway infrastructure managers to increase the capacity of the dense European railway network and to achieve cost reductions at the same time. Innovations developed to that effect rely heavily on digital technology. To cope with the ensued complexity, railway infrastructure managers are starting to appreciate more and more the use of formal modelling and verification techniques to support the development of these digital innovations. In my presentation I will discuss our contributions to two ongoing innovations in the railway domain: EULYNX and ERTMS/ETCS Hybrid Level 3.</p
SAT Solving with GPU Accelerated Inprocessing
Full text linkSince 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver ParaFROST solves many benchmarks faster on the GPU than its sequential counterparts
Resilient Capacity-Aware Routing
Full text linkTo ensure a high availability, communication networks provide resilient routing mechanisms that quickly change routes upon failures. However, a fundamental algorithmic question underlying such mechanisms is hardly understood: how to verify whether a given network reroutes flows along feasible paths, without violating capacity constraints, for up to k link failures? We chart the algorithmic complexity landscape of resilient routing under link failures, considering shortest path routing based on link weights as e.g. deployed in the ECMP protocol. We study two models: a pessimistic model where flows interfere in a worst-case manner along equal-cost shortest paths, and an optimistic model where flows are routed in a best-case manner, and we present a complete picture of the algorithmic complexities.We further propose a strategic search algorithm that checks only the critical failure scenarios while still providing correctness guarantees. Our experimental evaluation on a benchmark of Internet and datacenter topologies confirms an improved performance of our strategic search by several orders of magnitude
- …
