arXiv subjects

Jana Tumova

Publications and source records attributed to Jana Tumova.

52 records · Page 3Linked to original sources

arXiv2017

On the Timed Temporal Logic Planning of Coupled Multi-Agent Systems

This paper presents a fully automated procedure for controller synthesis for multi-agent systems under coupling constraints. Each agent is modeled with dynamics consisting of two terms: the first one models the coupling constraints and the other one is an additional bounded control input. We aim to design these inputs so that each agent meets an individual high-level specification given as a Metric Interval Temporal Logic (MITL). First, a decentralized abstraction that provides a space and time discretization of the multi-agent system is designed. Second, by utilizing this abstraction and techniques from formal verification, we propose an algorithm that computes the individual runs which provably satisfy the high-level tasks. The overall approach is demonstrated in a simulation example conducted in MATLAB environment.

eess.SY↗

arXiv2017

Probabilistic Plan Synthesis for Coupled Multi-Agent Systems

This paper presents a fully automated procedure for controller synthesis for multi-agent systems under the presence of uncertainties. We model the motion of each of the $N$ agents in the environment as a Markov Decision Process (MDP) and we assign to each agent one individual high-level formula given in Probabilistic Computational Tree Logic (PCTL). Each agent may need to collaborate with other agents in order to achieve a task. The collaboration is imposed by sharing actions between the agents. We aim to design local control policies such that each agent satisfies its individual PCTL formula. The proposed algorithm builds on clustering the agents, MDP products construction and controller policies design. We show that our approach has better computational complexity than the centralized case, which traditionally suffers from very high computational demands.

eess.SY↗

arXiv2017

Proceedings International Workshop on Formal Engineering approaches to Software Components and Architectures

These are the proceedings of the 14th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA). The workshop was held on April 22, 2017 in Uppsala (Sweden) as a satellite event to the European Joint Conference on Theory and Practice of Software (ETAPS'17). The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for software engineering. In recent years, the growing importance of functional correctness and the increased relevance of system quality properties (e.g. performance, reliability, security) have stimulated the emergence of analytical and modelling techniques for the design and development of software systems. With the increasing complexity and utilization of today's software systems, FESCA aims at addressing two research questions: (1) what role is played by the software design phase in the systematic addressing of the analytical and modelling challenges, and (2) how can formal and semi-formal techniques be effectively applied to make the issues easier to address automatically, with lower human intervention.

cs.SE↗

arXiv2016

Synthesizing least-limiting guidelines for safety of semi-autonomous systems

We consider the problem of synthesizing safe-by-design control strategies for semi-autonomous systems. Our aim is to address situations when safety cannot be guaranteed solely by the autonomous, controllable part of the system and a certain level of collaboration is needed from the uncontrollable part, such as the human operator. In this paper, we propose a systematic solution to generating least-limiting guidelines, i.e. the guidelines that restrict the human operator as little as possible in the worst-case long-term system executions. The algorithm leverages ideas from 2-player turn-based games.

eess.SY↗

arXiv2016

Decomposition of Multi-Agent Planning under Distributed Motion and Task LTL Specifications

The aim of this work is to introduce an efficient procedure for discrete multi-agent planning under local complex temporal logic behavior specifications. While the first part of an agent's behavior specification constraints the agent's trace and is independent, the second part of the specification expresses the agent's tasks in terms of the services to be provided along the trace and may impose requests for the other agents' collaborations. To fight the extreme computational complexity of centralized multi-agent planning, we propose a two-phase automata-based solution, where we systematically decouple the planning procedure for the two types of specifications. At first, we only consider the former specifications in a fully decentralized way and we compactly represent each agents' admissible traces by abstracting away the states that are insignificant for the satisfaction of their latter specifications. Second, the synchronized planning procedure uses only the compact representations. The satisfaction of the overall specification is guaranteed by construction for each agent. An illustrative example demonstrating the practical benefits of the solution is included.

eess.SY↗

arXiv2016

Multi-Agent Planning under Local LTL Specifications and Event-Based Synchronization

We study the problem of plan synthesis for multi-agent systems, to achieve complex, high-level, long-term goals that are assigned to each agent individually. As the agents might not be capable of satisfying their respective goals by themselves, requests for other agents' collaborations are a part of the task descriptions. We consider that each agent is modeled as a discrete state-transition system and its task specification takes a form of a linear temporal logic formula, which may contain requirements and constraints on the other agent's behavior. A traditional automata-based approach to multi-agent plan synthesis from such specifications builds on centralized team planning and full team synchronization after each agents' discrete step, and thus suffers from extreme computational demands. We aim at reducing the computational complexity by decomposing the plan synthesis problem into finite horizon planning problems that are solved iteratively, upon the run of the agents. As opposed to full synchronization, we introduce an event-based synchronization that allows our approach to efficiently adapt to different time durations of different agents' discrete steps. We discuss the correctness of the solution and find assumptions, under which the proposed iterative algorithm leads to provable eventual satisfaction of the desired specifications.

eess.SY↗

arXiv2016

Cooperative Planning for Coupled Multi-Agent Systems under Timed Temporal Specifications

This paper presents a fully automated procedure for controller synthesis for multi-agent systems under coupled constraints. Each agent has dynamics consisting of two terms: the first one models the coupled constraints and the other one is an additional control input. We aim to design these inputs so that each agent meets an individual high-level specification given as a Metric Interval Temporal Logic (MITL). First, a decentralized abstraction that provides a time and space discretization of the multi-agent system is designed. Second, by utilizing this abstraction and techniques from formal veri- fication, we provide an algorithm that computes the individual runs which provably satisfy the high-level tasks. The overall approach is demonstrated in a simulation example.

eess.SY↗

arXiv2016

Proceedings of the 13th International Workshop on Formal Engineering Approaches to Software Components and Architectures

The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for software engineering. In recent years, the growing importance of functional correctness and the increased relevance of system quality properties (e.g. performance, reliability, security) have stimulated the emergence of analytical and modelling techniques for the design and development of software systems. With the increasing complexity and utilization of today's software systems, FESCA aims at addressing two research questions: (1) what role is played by the software design phase in the systematic addressing of the analytical and modelling challenges, and (2) how can formal and semi-formal techniques be effectively applied to make the issues easier to address automatically, with lower human intervention. We encourage submissions on (semi-)formal techniques and their application that aid analysis, design and implementation of software applications, especially those employed in interconnected, communicating devices, devices interacting with the physical world, and cyber-physical systems.

cs.SE↗

arXiv2015

Cooperative Task Planning of Multi-Agent Systems Under Timed Temporal Specifications

In this paper the problem of cooperative task planning of multi-agent systems when timed constraints are imposed to the system is investigated. We consider timed constraints given by Metric Interval Temporal Logic (MITL). We propose a method for automatic control synthesis in a two-stage systematic procedure. With this method we guarantee that all the agents satisfy their own individual task specifications as well as that the team satisfies a team global task specification.

eess.SY↗

arXiv2014

Communication-Free Multi-Agent Control under Local Temporal Tasks and Relative-Distance Constraints

We propose a distributed control and coordination strategy for multi-agent systems where each agent has a local task specified as a Linear Temporal Logic (LTL) formula and at the same time is subject to relative-distance constraints with its neighboring agents. The local tasks capture the temporal requirements on individual agents' behaviors, while the relative-distance constraints impose requirements on the collective motion of the whole team. The proposed solution relies only on relative-state measurements among the neighboring agents without the need for explicit information exchange. It is guaranteed that the local tasks given as syntactically co-safe or general LTL formulas are fulfilled and the relative-distance constraints are satisfied at all time. The approach is demonstrated with computer simulations.

cs.MA↗

arXiv2014

Cooperative Decentralized Multi-agent Control under Local LTL Tasks and Connectivity Constraints

We propose a framework for the decentralized control of a team of agents that are assigned local tasks expressed as Linear Temporal Logic (LTL) formulas. Each local LTL task specification captures both the requirements on the respective agent's behavior and the requests for the other agents' collaborations needed to accomplish the task. Furthermore, the agents are subject to communication constraints. The presented solution follows the automata-theoretic approach to LTL model checking, however, it avoids the computationally demanding construction of synchronized product system between the agents. We suggest a decentralized coordination among the agents through a dynamic leader-follower scheme, to guarantee the low-level connectivity maintenance at all times and a progress towards the satisfaction of the leader's task. By a systematic leader switching, we ensure that each agent's task will be accomplished.

eess.SY↗

arXiv2014

A Receding Horizon Approach to Multi-Agent Planning from Local LTL Specifications

We study the problem of control synthesis for multi-agent systems, to achieve complex, high-level, long-term goals that are assigned to each agent individually. As the agents might not be capable of satisfying their respective goals by themselves, requests for other agents' collaborations are a part of the task descriptions. Particularly, we consider that the task specification takes a form of a linear temporal logic formula, which may contain requirements and constraints on the other agent's behavior. A traditional automata-based approach to multi-agent strategy synthesis from such specifications builds on centralized planning for the whole team and thus suffers from extreme computational demands. In this work, we aim at reducing the computational complexity by decomposing the strategy synthesis problem into short horizon planning problems that are solved iteratively, upon the run of the agents. We discuss the correctness of the solution and find assumptions, under which the proposed iterative algorithm leads to provable eventual satisfaction of the desired specifications.

cs.RO↗

arXiv2013

Incremental Sampling-based Algorithm for Minimum-violation Motion Planning

This paper studies the problem of control strategy synthesis for dynamical systems with differential constraints to fulfill a given reachability goal while satisfying a set of safety rules. Particular attention is devoted to goals that become feasible only if a subset of the safety rules are violated. The proposed algorithm computes a control law, that minimizes the level of unsafety while the desired goal is guaranteed to be reached. This problem is motivated by an autonomous car navigating an urban environment while following rules of the road such as "always travel in right lane'' and "do not change lanes frequently''. Ideas behind sampling based motion-planning algorithms, such as Probabilistic Road Maps (PRMs) and Rapidly-exploring Random Trees (RRTs), are employed to incrementally construct a finite concretization of the dynamics as a durational Kripke structure. In conjunction with this, a weighted finite automaton that captures the safety rules is used in order to find an optimal trajectory that minimizes the violation of safety rules. We prove that the proposed algorithm guarantees asymptotic optimality, i.e., almost-sure convergence to optimal solutions. We present results of simulation experiments and an implementation on an autonomous urban mobility-on-demand system.

cs.RO↗

arXiv2013

Minimum-violation LTL Planning with Conflicting Specifications

We consider the problem of automatic generation of control strategies for robotic vehicles given a set of high-level mission specifications, such as "Vehicle x must eventually visit a target region and then return to a base," "Regions A and B must be periodically surveyed," or "None of the vehicles can enter an unsafe region." We focus on instances when all of the given specifications cannot be reached simultaneously due to their incompatibility and/or environmental constraints. We aim to find the least-violating control strategy while considering different priorities of satisfying different parts of the mission. Formally, we consider the missions given in the form of linear temporal logic formulas, each of which is assigned a reward that is earned when the formula is satisfied. Leveraging ideas from the automata-based model checking, we propose an algorithm for finding an optimal control strategy that maximizes the sum of rewards earned if this control strategy is applied. We demonstrate the proposed algorithm on an illustrative case study.

cs.RO↗

arXiv2012

Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints

Our goal in this paper is to plan the motion of a robot in a partitioned environment with dynamically changing, locally sensed rewards. We assume that arbitrary assumptions on the reward dynamics can be given. The robot aims to accomplish a high-level temporal logic surveillance mission and to locally optimize the collection of the rewards in the visited regions. These two objectives often conflict and only a compromise between them can be reached. We address this issue by taking into consideration a user-defined preference function that captures the trade-off between the importance of collecting high rewards and the importance of making progress towards a surveyed region. Our solution leverages ideas from the automata-based approach to model checking. We demonstrate the utilization and benefits of the suggested framework in an illustrative example.

cs.RO↗

arXiv2010

Optimal Path Planning under Temporal Logic Constraints

In this paper we present a method for automatically generating optimal robot trajectories satisfying high level mission specifications. The motion of the robot in the environment is modeled as a general transition system, enhanced with weighted transitions. The mission is specified by a general linear temporal logic formula. In addition, we require that an optimizing proposition must be repeatedly satisfied. The cost function that we seek to minimize is the maximum time between satisfying instances of the optimizing proposition. For every environment model, and for every formula, our method computes a robot trajectory which minimizes the cost function. The problem is motivated by applications in robotic monitoring and data gathering. In this setting, the optimizing proposition is satisfied at all locations where data can be uploaded, and the entire formula specifies a complex (and infinite horizon) data collection mission. Our method utilizes Büchi automata to produce an automaton (which can be thought of as a graph) whose runs satisfy the temporal logic specification. We then present a graph algorithm which computes a path corresponding to the optimal robot trajectory. We also present an implementation for a robot performing a data gathering mission in a road network.

cs.RO↗