Showing 1–15 of 15 results for author: Fabian, M

A Comparative Study of SMT and MILP for the Nurse Rostering Problem

Authors: Alvin Combrink, Stephie Do, Kristofer Bengtsson, Sabino Francesco Roselli, Martin Fabian

Abstract: The effects of personnel scheduling on the quality of care and working conditions for healthcare personnel have been thoroughly documented. However, the ever-present demand and large variation of constraints make healthcare scheduling particularly challenging. This problem has been studied for decades, with limited research aimed at applying Satisfiability Modulo Theories (SMT). SMT has gained mom… ▽ More The effects of personnel scheduling on the quality of care and working conditions for healthcare personnel have been thoroughly documented. However, the ever-present demand and large variation of constraints make healthcare scheduling particularly challenging. This problem has been studied for decades, with limited research aimed at applying Satisfiability Modulo Theories (SMT). SMT has gained momentum within the formal verification community in the last decades, leading to the advancement of SMT solvers that have been shown to outperform standard mathematical programming techniques. In this work, we propose generic constraint formulations that can model a wide range of real-world scheduling constraints. Then, the generic constraints are formulated as SMT and MILP problems and used to compare the respective state-of-the-art solvers, Z3 and Gurobi, on academic and real-world inspired rostering problems. Experimental results show how each solver excels for certain types of problems; the MILP solver generally performs better when the problem is highly constrained or infeasible, while the SMT solver performs better otherwise. On real-world inspired problems containing a more varied set of shifts and personnel, the SMT solver excels. Additionally, it was noted during experimentation that the SMT solver was more sensitive to the way the generic constraints were formulated, requiring careful consideration and experimentation to achieve better performance. We conclude that SMT-based methods present a promising avenue for future research within the domain of personnel scheduling. △ Less

Submitted 15 May, 2025; originally announced May 2025.

Comments: 6 pages, 3 figures

Prioritized Planning for Continuous-time Lifelong Multi-agent Pathfinding

Authors: Alvin Combrink, Sabino Francesco Roselli, Martin Fabian

Abstract: Multi-agent Path Finding (MAPF) is the problem of planning collision-free movements of agents such that they get from where they are to where they need to be. Commonly, agents are located on a graph and can traverse edges. This problem has many variations and has been studied for decades. Two such variations are the continuous-time and the lifelong MAPF problems. In the continuous-time MAPF proble… ▽ More Multi-agent Path Finding (MAPF) is the problem of planning collision-free movements of agents such that they get from where they are to where they need to be. Commonly, agents are located on a graph and can traverse edges. This problem has many variations and has been studied for decades. Two such variations are the continuous-time and the lifelong MAPF problems. In the continuous-time MAPF problem, edges can have non-unit lengths and agents can traverse them at any real-valued time. Additionally, agent volumes are often included. In the lifelong MAPF problem, agents must attend to a continuous stream of incoming tasks. Much work has been devoted to designing solution methods within these two areas. However, to our knowledge, the combined problem of continuous-time lifelong MAPF has yet to be addressed. This work addresses continuous-time lifelong MAPF with agent volumes by presenting the fast and sub-optimal Continuous-time Prioritized Lifelong Planner (CPLP). CPLP continuously re-prioritizes tasks, assigns agents to them, and computes agent plans using a combination of two path planners; one based on CCBS and the other on SIPP. Experimental results with up to $400$ agents on graphs with $4000$ vertices demonstrate average computation times below $20$ ms per call. In online settings where available time to compute plans is limited, CPLP ensures collision-free movement even when failing to meet these time limits. Therefore, the robustness of CPLP highlights its potential for real-world applications. △ Less

Submitted 17 March, 2025; originally announced March 2025.

Identification of Minimally Restrictive Assembly Sequences using Supervisory Control Theory

Authors: Martina Vinetti, Martin Fabian

Abstract: Modern assembly processes require flexibility and adaptability to handle increasing product variety and customization. Traditional assembly planning methods often prioritize finding an optimal assembly sequence, overlooking the requirements of contemporary manufacturing. This work uses Supervisory Control Theory to systematically generate all feasible assembly sequences while ensuring compliance w… ▽ More Modern assembly processes require flexibility and adaptability to handle increasing product variety and customization. Traditional assembly planning methods often prioritize finding an optimal assembly sequence, overlooking the requirements of contemporary manufacturing. This work uses Supervisory Control Theory to systematically generate all feasible assembly sequences while ensuring compliance with precedence and process constraints. By synthesizing a controllable, non-blocking, and minimally restrictive supervisor, the proposed method guarantees that only valid sequences are allowed, balancing flexibility and constraint enforcement. The obtained sequences can serve as a basis for further optimization or exception management, improving responsiveness to disruptions. △ Less

Submitted 7 March, 2025; originally announced March 2025.

A Formal-Methods Approach to Provide Evidence in Automated-Driving Safety Cases

Authors: Jonas Krook, Yuvaraj Selvaraj, Wolfgang Ahrendt, Martin Fabian

Abstract: The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads. This persuasion is typically facilitated by compiling the arguments and the compelling evidence into a safety case. Reviews and testing, two common approaches to e… ▽ More The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads. This persuasion is typically facilitated by compiling the arguments and the compelling evidence into a safety case. Reviews and testing, two common approaches to ensure correctness of automotive systems cannot explore the typically infinite set of possible behaviours. In contrast, formal methods are exhaustive methods that can provide mathematical proofs of correctness of models, and they can be used to prove that formalizations of functional safety requirements are fulfilled by formal models of system components. This paper shows how formal methods can provide evidence for the correct break-down of the functional safety requirements onto the components that are part of feedback loops, and how this evidence fits into the argument of the safety case. If a proof is obtained, the formal models are used as requirements on the components. This structure of the safety argumentation can be used to alleviate the need for reviews and tests to ensure that the break-down is correct, thereby saving effort both in data collection and verification time. △ Less

Submitted 13 October, 2022; originally announced October 2022.

Comments: 8 pages, 3 figures. This work has been submitted to the IEEE for possible publication

On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic

Authors: Yuvaraj Selvaraj, Jonas Krook, Wolfgang Ahrendt, Martin Fabian

Abstract: Cyber-physical systems are often safety-critical and their correctness is crucial, as in the case of automated driving. Using formal mathematical methods is one way to guarantee correctness. Though these methods have shown their usefulness, care must be taken as modeling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. This paper deals with tw… ▽ More Cyber-physical systems are often safety-critical and their correctness is crucial, as in the case of automated driving. Using formal mathematical methods is one way to guarantee correctness. Though these methods have shown their usefulness, care must be taken as modeling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. This paper deals with two such modeling errors in differential dynamic logic. Differential dynamic logic is a formal specification and verification language for hybrid systems, which are mathematical models of cyber-physical systems. The main contribution is to prove conditions that when fulfilled, these two modeling errors cannot cause a faulty controller to be proven safe. The problems are illustrated with a real world example of a safety controller for automated driving, and it is shown that the formulated conditions have the intended effect both for a faulty and a correct controller. It is also shown how the formulated conditions aid in finding a loop invariant candidate to prove properties of hybrid systems with feedback loops. The results are proven using the interactive theorem prover KeYmaera X. △ Less

Submitted 12 July, 2022; originally announced July 2022.

snapshot CEST++ : the next snapshot CEST for fast whole-brain APTw imaging at 3T

Authors: Patrick Liebig, Maria Sedykh, Kai Herz, Moritz S. Fabian, Angelika Mennecke, Simon Weinmüller, Manuel Schmidt, Arnd Dörfler, Moritz Zaiss

Abstract: CEST suffers from two main problems long acquisitin times or restricted coverage as well as incoherent protocol settings. In this paper we give suggestions on how to optimise your protocol settings fro CEST and present one setting for APT CEST. To increase the coverage while keeping the acquisition time constant we suggest using a spatial temporal Compressed Sensing approach. Finally, 1.8mm isotro… ▽ More CEST suffers from two main problems long acquisitin times or restricted coverage as well as incoherent protocol settings. In this paper we give suggestions on how to optimise your protocol settings fro CEST and present one setting for APT CEST. To increase the coverage while keeping the acquisition time constant we suggest using a spatial temporal Compressed Sensing approach. Finally, 1.8mm isotropic whole brain APT CEST maps can be acquired in a little bit less than 2min with a fully integrated online reconstruction. This will pave the way to an even further clinical use of CEST. △ Less

Submitted 1 July, 2022; originally announced July 2022.

Robust Stutter Bisimulation for Abstraction and Controller Synthesis with Disturbance: Proofs

Authors: Jonas Krook, Robi Malik, Sahar Mohajerani, Martin Fabian

Abstract: This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of… ▽ More This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of the original system and then synthesise a controller for the abstract system. For this approach, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers for any given linear temporal logic formula. States are related by the robust stutter bisimulation relation if the same target sets can be guaranteed to be reached or avoided under control of some controllers, thereby ensuring that disturbances have similar effect on paths that start in related states. This paper presents an algorithm to construct the corresponding robust stutter bisimulation quotient to solve the abstraction problem, and it is shown, by explicit construction, that there exists a controller enforcing a linear temporal logic formula for the original system if and only if a corresponding controller exists for the quotient system. Lastly, the result of the algorithm and the controller construction are demonstrated by application to an example of robot navigation. △ Less

Submitted 27 May, 2022; originally announced May 2022.

Comments: 21 pages, 5 figures, Preprint submitted to Automatica, plus appendices with proofs of theorems

Formal Development of Safe Automated Driving using Differential Dynamic Logic

Authors: Yuvaraj Selvaraj, Wolfgang Ahrendt, Martin Fabian

Abstract: The challenges in providing convincing arguments for safe and correct behavior of automated driving (AD) systems have so far hindered their widespread commercial deployment. Conventional development approaches such as testing and simulation are limited by non-exhaustive analysis, and can thus not guarantee correctness in all possible scenarios. Formal methods is an approach to provide mathematical… ▽ More The challenges in providing convincing arguments for safe and correct behavior of automated driving (AD) systems have so far hindered their widespread commercial deployment. Conventional development approaches such as testing and simulation are limited by non-exhaustive analysis, and can thus not guarantee correctness in all possible scenarios. Formal methods is an approach to provide mathematical proofs of correctness, using a model of a system, that could be used to give the necessary arguments. This paper investigates the use of differential dynamic logic and the deductive verification tool KeYmaera X in the development of an AD feature. Specifically, formal models and safety proofs of different design variants of a Decision & Control module for an in-lane AD feature are presented. In doing so, the assumptions and invariant conditions necessary to guarantee safety are identified, and the paper shows how such an analysis helps during the development process in requirement refinement and formulation of the operational design domain. Furthermore, it is shown how the performance of the different models is formally analyzed exhaustively, in all their allowed behaviors. △ Less

Submitted 14 April, 2022; originally announced April 2022.

A Compositional Algorithm for the Conflict-Free Electric Vehicle Routing Problem

Authors: Sabino Francesco Roselli, Per-Lage Götvall, Martin Fabian, Knut Åkesson

Abstract: The Conflict-Free Electric Vehicle Routing Problem (CF-EVRP) is an extension of the Vehicle Routing Problem (VRP), a combinatorial optimization problem of designing routes for vehicles to visit customers such that a cost function, typically the number of vehicles or the total travelled distance, is minimized. The problem finds many logistics applications, particularly for highly automated logistic… ▽ More The Conflict-Free Electric Vehicle Routing Problem (CF-EVRP) is an extension of the Vehicle Routing Problem (VRP), a combinatorial optimization problem of designing routes for vehicles to visit customers such that a cost function, typically the number of vehicles or the total travelled distance, is minimized. The problem finds many logistics applications, particularly for highly automated logistic systems for material handling. The CF-EVRP involves constraints such as time windows on the delivery to the customers, limited operating range of the vehicles, and limited capacity on the number of vehicles that a road segment can accommodate at the same time. In this paper, the compositional algorithm ComSat for solving the CF-EVRP is presented. The algorithm iterates through the sub-problems until a globally feasible solution is found. The proposed algorithm is implemented using an optimizing SMT-solver and is evaluated against an implementation of a previously presented monolithic model. The soundness and completeness of the algorithm are proven, and it is benchmarked on a set of generated problems and found to be able to solve problems of industrial size. △ Less

Submitted 14 March, 2022; originally announced March 2022.

Towards Super-Resolution CEST MRI for Visualization of Small Structures

Authors: Lukas Folle, Katharian Tkotz, Fasil Gadjimuradov, Lorenz Kapsner, Moritz Fabian, Sebastian Bickelhaupt, David Simon, Arnd Kleyer, Gerhard Krönke, Moritz Zaiß, Armin Nagel, Andreas Maier

Abstract: The onset of rheumatic diseases such as rheumatoid arthritis is typically subclinical, which results in challenging early detection of the disease. However, characteristic changes in the anatomy can be detected using imaging techniques such as MRI or CT. Modern imaging techniques such as chemical exchange saturation transfer (CEST) MRI drive the hope to improve early detection even further through… ▽ More The onset of rheumatic diseases such as rheumatoid arthritis is typically subclinical, which results in challenging early detection of the disease. However, characteristic changes in the anatomy can be detected using imaging techniques such as MRI or CT. Modern imaging techniques such as chemical exchange saturation transfer (CEST) MRI drive the hope to improve early detection even further through the imaging of metabolites in the body. To image small structures in the joints of patients, typically one of the first regions where changes due to the disease occur, a high resolution for the CEST MR imaging is necessary. Currently, however, CEST MR suffers from an inherently low resolution due to the underlying physical constraints of the acquisition. In this work we compared established up-sampling techniques to neural network-based super-resolution approaches. We could show, that neural networks are able to learn the mapping from low-resolution to high-resolution unsaturated CEST images considerably better than present methods. On the test set a PSNR of 32.29dB (+10%), a NRMSE of 0.14 (+28%), and a SSIM of 0.85 (+15%) could be achieved using a ResNet neural network, improving the baseline considerably. This work paves the way for the prospective investigation of neural networks for super-resolution CEST MRI and, followingly, might lead to a earlier detection of the onset of rheumatic diseases. △ Less

Submitted 3 December, 2021; originally announced December 2021.

Journal ref: Proceedings, German Workshop on Medical Image Computing (2022) 210-215

An SMT Based Compositional Algorithm to Solve a Conflict-Free Electric Vehicle Routing Problem

Authors: Sabino Francesco Roselli, Martin Fabian, Knut Åkesson

Abstract: The Vehicle Routing Problem (VRP) is the combinatorial optimization problem of designing routes for vehicles to visit customers in such a fashion that a cost function, typically the number of vehicles, or the total travelled distance is minimized. The problem finds applications in industrial scenarios, for example where Automated Guided Vehicles run through the plant to deliver components from the… ▽ More The Vehicle Routing Problem (VRP) is the combinatorial optimization problem of designing routes for vehicles to visit customers in such a fashion that a cost function, typically the number of vehicles, or the total travelled distance is minimized. The problem finds applications in industrial scenarios, for example where Automated Guided Vehicles run through the plant to deliver components from the warehouse. This specific problem, henceforth called the Electric Conflict-Free Vehicle Routing Problem (CF-EVRP), involves constraints such as limited operating range of the vehicles, time windows on the delivery to the customers, and limited capacity on the number of vehicles the road segments can accommodate at the same time. Such a complex system results in a large model that cannot easily be solved to optimality in reasonable time. We therefore developed a compositional model that breaks down the problem into smaller and simpler sub-problems and provides sub-optimal, feasible solutions to the original problem. The algorithm exploits the strengths of SMT solvers, which proved in our previous work to be an efficient approach to deal with scheduling problems. Compared to a monolithic model for the CF-EVRP, written in the SMT standard language and solved using a state-of-the-art SMT solver the compositional model was found to be significantly faster. △ Less

Submitted 30 June, 2021; v1 submitted 10 June, 2021; originally announced June 2021.

Leveraging Conflicting Constraints in Solving Vehicle Routing Problems

Authors: Sabino Francesco Roselli, Remco Vader, Martin Fabian, Knut Akesson

Abstract: The Conflict-Free Electric Vehicle Routing Problem (CF-EVRP) is a combinatorial optimization problem of designing routes for vehicles to visit customers such that a cost function, typically the number of vehicles or the total travelled distance, is minimized. The CF-EVRP involves constraints such as time windows on the delivery to the customers, limited operating range of the vehicles, and limited… ▽ More The Conflict-Free Electric Vehicle Routing Problem (CF-EVRP) is a combinatorial optimization problem of designing routes for vehicles to visit customers such that a cost function, typically the number of vehicles or the total travelled distance, is minimized. The CF-EVRP involves constraints such as time windows on the delivery to the customers, limited operating range of the vehicles, and limited capacity on the number of vehicles that a road segment can simultaneously accommodate. In previous work, the compositional algorithm ComSat was introduced and that solves the CF-EVRP by breaking it down into sub-problems and iteratively solve them to build an overall solution. Though ComSat showed good performance in general, some problems took significant time to solve due to the high number of iterations required to find solutions that satisfy the road segments' capacity constraints. The bottleneck is the Path Changing Problem, i.e., the sub-problem of finding a new set of shortest paths to connect a subset of the customers, disregarding previously found shortest paths. This paper presents an improved version of the PathsChanger function to solve the Path Changing Problem that exploits the unsatisfiable core, i.e., information on which constraints conflict, to guide the search for feasible solutions. Experiments show faster convergence to feasible solutions compared to the previous version of PathsChanger. △ Less

Submitted 12 September, 2022; v1 submitted 15 March, 2021; originally announced March 2021.

Supervisory Control Synthesis of Timed Automata Using Forcible Events

Authors: Aida Rashidinejad, Michel Reniers, Martin Fabian

Abstract: Considering real-valued clocks in timed automata (TA) makes it a practical modeling framework for discrete-event systems. However, the infinite state space brings challenges to the control of TA. To synthesize a supervisor for TA using the conventional supervisory control theory, existing methods abstract TA to finite automata (FA). For many applications, the abstraction of real-time values result… ▽ More Considering real-valued clocks in timed automata (TA) makes it a practical modeling framework for discrete-event systems. However, the infinite state space brings challenges to the control of TA. To synthesize a supervisor for TA using the conventional supervisory control theory, existing methods abstract TA to finite automata (FA). For many applications, the abstraction of real-time values results in an explosion in the state space of FA. This paper presents a supervisory control synthesis algorithm directly applicable to the TA without any abstraction. The plant is given as a TA with a set of uncontrollable events and a set of forcible events. Forcible events can preempt the passage of time when needed. The synthesis algorithm works by iteratively strengthening the guards of edges labeled by controllable events and invariants of locations where the progression of time can be preempted by forcible events. The synthesized supervisor, which is also a TA, is guaranteed to be controllable, maximally permissive, and results in a nonblocking and safe supervised plant. △ Less

Submitted 18 February, 2021; originally announced February 2021.

Networked Supervisory Control Synthesis of Timed Discrete-Event Systems

Authors: Aida Rashidinejad, Michel Reniers, Martin Fabian

Abstract: Conventional supervisory control theory assumes full synchronization between the supervisor and the plant. This assumption is violated in a networked-based communication setting due to the presence of delays, and this may result in incorrect behavior of a supervisor obtained from conventional supervisory control theory. This paper presents a technique to synthesize a networked supervisor handling… ▽ More Conventional supervisory control theory assumes full synchronization between the supervisor and the plant. This assumption is violated in a networked-based communication setting due to the presence of delays, and this may result in incorrect behavior of a supervisor obtained from conventional supervisory control theory. This paper presents a technique to synthesize a networked supervisor handling communication delays. For this purpose, first, a networked supervisory control framework is provided, where the supervisor interacts with the plant through control and observation channels, both of which introduce delays. The control channel is FIFO, but the observation channel is assumed to be non-FIFO so that the observation of events may not necessarily be received by the supervisor in the same order as they occurred in the plant. It is assumed that a global clock exists in the networked control system, and so the communication delays are represented in terms of time. Based on the proposed framework, a networked plant automaton is achieved, which models the behavior of the plant under the effects of communication delays and disordered observations. Based on the networked plant, the networked supervisor is synthesized, which is guaranteed to be (timed networked) controllable, nonblocking, time-lock free, (timed networked) maximally permissive, and satisfies control requirements for the plant. △ Less

Submitted 18 February, 2021; originally announced February 2021.

Model Properties for Efficient Synthesis of Nonblocking Modular Supervisors

Authors: Martijn Goorden, Joanna van de Mortel-Fronczak, Michel Reniers, Martin Fabian, Wan Fokkink, Jacobus Rooda

Abstract: Supervisory control theory provides means to synthesize supervisors for systems with discrete-event behavior from models of the uncontrolled plant and of the control requirements. The applicability of supervisory control theory often fails due to a lack of scalability of the algorithms. The paper proposes a format for the requirements and a method to ensure that the crucial properties of controlla… ▽ More Supervisory control theory provides means to synthesize supervisors for systems with discrete-event behavior from models of the uncontrolled plant and of the control requirements. The applicability of supervisory control theory often fails due to a lack of scalability of the algorithms. The paper proposes a format for the requirements and a method to ensure that the crucial properties of controllability and nonblockingness directly hold, thus avoiding the most computationally expensive parts of synthesis. The method consists of creating a control problem dependency graph and verifying whether it is acyclic. Vertices of the graph are modular plant components, and edges are derived from the requirements. In case of a cyclic graph, potential blocking issues can be localized, so that the original control problem can be reduced to only synthesizing supervisors for smaller partial control problems. The strength of the method is illustrated on two case studies: a production line and a roadway tunnel. △ Less

Submitted 16 April, 2021; v1 submitted 11 July, 2020; originally announced July 2020.

Comments: Submitted to Journal of Control Engineering Practice, revision 2