arXiv subjects

Martin Fabian

Publications and source records attributed to Martin Fabian.

At least 19 recordsLinked to original sources

arXiv2026

AOC-CBS: Anytime-Optimal Continuous-time Conflict-Based Search for Generalised Multi-Agent Path Finding

Many research fields share a common structure: a set of agents, each pursuing its own goal, whose actions must be coordinated so that no two of them conflict. Multi-Agent Path Finding (MAPF) is a concrete instance of this structure, with applications from warehouses to road traffic and airports. Much of MAPF research assumes discrete time, circular agents sharing one spatial graph, a single goal per agent, and that an agent must remain at its goal once reached, precluding heterogeneous fleets, non-geometric conflicts, task sequences, and agents that move on after completing them. We generalise the MAPF formulation to lift these assumptions, and present Anytime-Optimal Continuous-time Conflict-Based Search (AOC-CBS), an exact and solution-complete solver for it. AOC-CBS guarantees the eventual return of an optimal solution, while reporting an incumbent with a known optimality gap upper bound throughout its runtime; it is configurable with a portfolio of repair functions, one of which we introduce (Tier-Prioritized Safe Interval Path Planning), and can exploit multiple processor cores. We demonstrate AOC-CBS on a mixed fleet of non-convex agents moving along smooth, kinodynamically feasible trajectories. Preliminary experiments against the exact solver OC-CBS, on well-known benchmarks and roadmaps we sample from them, show AOC-CBS is comparable at finding optimal solutions while extending scalability from the tens to the hundreds of agents when a bounded optimality gap is accepted.

cs.MA↗

arXiv2026

Multi-Worker Assembly Line Rebalancing with Relevance-Guided Configuration Preservation

In assembly line balancing, tasks are assigned to stations in order to satisfy a required cycle time. When production conditions change, the line must be rebalanced by modifying the current task allocation, typically aiming to move as few tasks as possible between stations. Similarity measures are commonly used to control such changes, but they generally evaluate configuration preservation by treating all tasks equally, which may not reflect their different practical importance. In this work, a \emph{pruned Mean Similarity Factor} is proposed for assembly line rebalancing, evaluating similarity only over a subset of structurally relevant tasks identified through a relevance score. The proposed measure is integrated into a compact mixed-integer linear programming (MILP) formulation that considers practical aspects of manual assembly, specifically workload balance, ergonomic exposure, multi-worker stations, and positional constraints. Computational experiments on extended benchmark instances derived from the literature show that the proposed approach can obtain optimal rebalancing solutions within reasonable computational times, while maintaining high task colocation and balanced workload and ergonomic distributions. In particular, focusing the similarity evaluation on relevant tasks helps reduce the computational effort.

eess.SY↗

arXiv2026

A General Formulation for the Teaching Assignment Problem: Computational Analysis Over a Real-World Dataset

The Teacher Assignment Problem is a combinatorial optimization problem that involves assigning teachers to courses while guaranteeing that all courses are covered, teachers do not teach too few or too many hours, teachers do not switch assigned courses too often and possibly teach the courses they favor. Typically the problem is solved manually, a task that requires several hours every year. In this work we present a mathematical formulation for the problem and an experimental evaluation of the model implemented using state-of-the-art SMT, CP, and MILP solvers. The implementations are tested over a real-world dataset provided by the Division of Systems and Control at Chalmers University of Technology, and produce teacher assignments with smaller workload deviation, a more even workload distribution among the teachers, and a lower number of switched courses.

eess.SY↗

arXiv2025

A Multi-Worker Assembly Line Rebalancing with Spatial and Ergonomic Considerations

This work addresses the Assembly Line Rebalancing Problem driven by cycle-time changes in manual assembly systems where multiple workers operate in parallel within the same station. A multi-objective optimization model is proposed that incorporates task reassignment, worker allocation, ergonomic evaluation, and explicit spatial feasibility through work-area constraints. The formulation minimizes deviations from the current configuration while promoting balanced workload and ergonomic conditions among workers. The main contribution is the extension of assembly line rebalancing to multi-worker settings with explicit spatial constraints. Computational experiments on synthetic instances demonstrate that the model consistently generates feasible reconfigurations, highlighting its potential as a decision-support tool for industrial rebalancing in flexible production environments.

eess.SY↗

arXiv2025

Optimal Multi-Agent Path Finding in Continuous Time

Continuous-time Conflict Based Search (CCBS) has been widely used as an exact baseline for Continuous-time Multi-Agent Path Finding (MAPFR), and its correctness guarantees underpin a range of continuation methods built on top of it. Recent work, however, has shown that CCBS's guarantees of exactness and solution completeness do not in fact hold: optimal solutions can be removed from the search, causing the algorithm to return suboptimal solutions. This paper establishes sufficient conditions for exactness and solution completeness in CCBS-style algorithms, and introduces Optimal Continuous-time Conflict-Based Search (OC-CBS) which satisfies these conditions. OC-CBS therefore guarantees an optimal solution on every solvable MAPFR instance. Experiments on benchmark problems show that OC-CBS remains competitive with CCBS in runtime while providing formal correctness guarantees. Because OC-CBS is a drop-in replacement for CCBS, it also restores the theoretical guarantees of existing methods that relied on CCBS's now-invalidated correctness. Finally, the framework and correctness criteria offer a general foundation for analyzing and designing future exact MAPFR solvers.

cs.MA↗

arXiv2025

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

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.

cs.AI↗

arXiv2025

Prioritized Planning for Continuous-time Lifelong Multi-agent Pathfinding

Multi-agent Path Finding (MAPF) is the problem of planning collision-free movements of agents so 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 former, edges have non-unit lengths and volumetric agents can traverse them at any real-valued time. In the latter, agents must attend to a continuous stream of incoming tasks. Much work has been devoted to designing solution methods within these two areas. To our knowledge, however, the combined problem of continuous-time lifelong MAPF has yet to be addressed. This work addresses continuous-time lifelong MAPF with volumetric agents by presenting the fast and sub-optimal Continuous-time Prioritized Lifelong Planner (CPLP). CPLP continuously assigns agents to tasks and computes plans using a combination of two path planners; one based on CCBS and the other based on SIPP. Experimental results with up to 800 agents on graphs with up to 12 000 vertices demonstrate practical performance, where maximum planning times fall within the available time budget. Additionally, CPLP ensures collision-free movement even when failing to meet this budget. Therefore, the robustness of CPLP highlights its potential for real-world applications.

eess.SY↗

arXiv2025

Identification of Minimally Restrictive Assembly Sequences using Supervisory Control Theory

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.

eess.SY↗

arXiv2022

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

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.

cs.SE↗

arXiv2022

Hazard Analysis of Collaborative Automation Systems: A Two-layer Approach based on Supervisory Control and Simulation

Safety critical systems are typically subjected to hazard analysis before commissioning to identify and analyse potentially hazardous system states that may arise during operation. Currently, hazard analysis is mainly based on human reasoning, past experiences, and simple tools such as checklists and spreadsheets. Increasing system complexity makes such approaches decreasingly suitable. Furthermore, testing-based hazard analysis is often not suitable due to high costs or dangers of physical faults. A remedy for this are model-based hazard analysis methods, which either rely on formal models or on simulation models, each with their own benefits and drawbacks. This paper proposes a two-layer approach that combines the benefits of exhaustive analysis using formal methods with detailed analysis using simulation. Unsafe behaviours that lead to unsafe states are first synthesised from a formal model of the system using Supervisory Control Theory. The result is then input to the simulation where detailed analyses using domain-specific risk metrics are performed. Though the presented approach is generally applicable, this paper demonstrates the benefits of the approach on an industrial human-robot collaboration system.

cs.RO↗

arXiv2022

Leveraging Conflicting Constraints in Solving Vehicle Routing Problems

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.

eess.SY↗

arXiv2022

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

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.

eess.SY↗

arXiv2022

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

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.

eess.SY↗

arXiv2022

Formal Development of Safe Automated Driving using Differential Dynamic Logic

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.

eess.SY↗

arXiv2022

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

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.

eess.SY↗

arXiv2021

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

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.

cs.AI↗

arXiv2021

Model Properties for Efficient Synthesis of Nonblocking Modular Supervisors

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.

eess.SY↗

arXiv2021

Networked Supervisory Control Synthesis of Timed Discrete-Event Systems

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.

eess.SY↗