BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Martin Fabian

Martin Fabian contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
eess.SYSystems and ControlFormal Languages and Automata Theorymath.LO

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
7works
0followers
4topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

7 published item(s)

preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Supervisory Control Synthesis of Timed Automata Using Forcible Events

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.

0 citations0 reviewsNo code linkedOpen access