Author name cluster

Eugene Asarin

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

I&C Journal 2015 Journal Article

Entropy of regular timed languages

Eugene Asarin
Nicolas Basset
Aldric Degorre

To study the size of regular timed languages, we generalize a classical approach introduced by Chomsky and Miller for discrete automata: count words having n symbols, and compute the exponential growth rate of their number (entropy). For timed automata, we replace cardinality by volume and define (volumetric) entropy similarly. It represents the average quantity of information per event in a timed word of the language. We exhibit a criterion for telling apart “thick” timed automata with non-vanishing entropy, for which typical runs are non-Zeno and discretizable, from “thin” automata for which all runs behave in a Zeno-like way, implying a quick volume collapse. We associate to every timed automaton a positive integral operator; the entropy equals the logarithm of its spectral radius. This operator has a spectral gap, thus allowing for fast converging numerical procedures to approximate entropy. In a special case, entropy is even characterized symbolically.

Details DOI

MFCS Conference 2012 Conference Paper

Generating Functions of Timed Languages

Eugene Asarin
Nicolas Basset
Aldric Degorre
Dominique Perrin

Abstract In order to study precisely the growth of timed languages, we associate to such a language a generating function. These functions (tightly related to volume and entropy of timed languages) satisfy compositionality properties and, for deterministic timed regular languages, can be characterized by integral equations. We provide procedures for closed-form computation of generating functions for some classes of timed automata and regular expressions.

Details

I&C Journal 2012 Journal Article

Low dimensional hybrid systems – decidable, undecidable, donʼt know

Eugene Asarin
Venkatesh P. Mysore
Amir Pnueli
Gerardo Schneider

Even though many attempts have been made to define the boundary between decidable and undecidable hybrid systems, the affair is far from being resolved. More and more low dimensional systems are being shown to be undecidable with respect to reachability, and many open problems in between are being discovered. In this paper, we present various two-dimensional hybrid systems for which the reachability problem is undecidable. We show their undecidability by simulating Minsky machines. Their proximity to the decidability frontier is understood by inspecting the most parsimonious constraints necessary to make reachability over these automata decidable. We also show that for other two-dimensional systems, the reachability question remains unanswered, by proving that it is as hard as the reachability problem for piecewise affine maps on the real line, which is a well known open problem.

Details DOI

TIME Conference 2009 Conference Paper

Simple Algorithm for Simple Timed Games

Yasmina Abdeddaïm
Eugene Asarin
Mihaela Sighireanu

We propose a subclass of timed game automata(TGA), called Task TGA, representing networks of communicating tasks where the system can choose when to start the task and the environment can choose the duration of the task. We search to solve finite-horizon reachability games on Task TGA by building strategies in the form of Simple Temporal Networks with Uncertainty (STNU). Such strategies have the advantage of being very succinct due to the partial order reduction of independent tasks. We show that the existence of such strategies is an NP-complete problem. A practical consequence of this result is a fully forward algorithm for building STNU strategies. Potential applications of this work are planning and scheduling under temporal uncertainty.

Details

TCS Journal 2008 Journal Article

Algorithmic analysis of polygonal hybrid systems, Part II: Phase portrait and tools

Eugene Asarin
Gordon Pace
Gerardo Schneider
Sergio Yovine

Polygonal differential inclusion systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as the computation of certain objects of the phase portrait is decidable. In this paper we show how to compute the viability, controllability and invariance kernels, as well as semi-separatrix curves for SPDIs. We also present the tool SPeeDI+, which implements a reachability algorithm and computes phase portraits of SPDIs.

Details DOI

TCS Journal 2007 Journal Article

Algorithmic analysis of polygonal hybrid systems, part I: Reachability

Eugene Asarin
Gerardo Schneider
Sergio Yovine

In this work we are concerned with the formal verification of two-dimensional non-deterministic hybrid systems, namely polygonal differential inclusion systems (SPDIs). SPDIs are a class of non-deterministic systems that correspond to piecewise constant differential inclusions on the plane, for which we study the reachability problem. Our contribution is the development of an algorithm for solving exactly the reachability problem of SPDIs. We extend the geometric approach due to Maler and Pnueli [O. Maler, A. Pnueli. Reachability analysis of planar multi-linear systems. in: C. Courcoubetis (Ed.), CAV’93, in: LNCS, vol. 697, Springer-Verlag, 1993, pp. 194–209] to non-deterministic systems, based on the combination of three techniques: the representation of the two-dimensional continuous-time dynamics as a one-dimensional discrete-time system (using Poincaré maps), the characterization of the set of qualitative behaviors of the latter as a finite set of types of signatures, and acceleration used to explore reachability according to each of these types.

Details DOI

ICAPS Conference 2007 Conference Paper

Planning Robust Temporal Plans: A Comparison Between CBTP and TGA Approaches

Yasmina Abdeddaïm
Eugene Asarin
Matthieu Gallien
Félix Ingrand
Charles Lesire
Mihaela Sighireanu

Planning for real world applications, with explicit temporal representation and a robust execution is a very challenging problem. To tackle it, the planning community has proposed a number of original and successful approaches. However, there are other paradigms "outside" the Automated Planning field which may prove to be successful with respect to this objective. This paper presents a comparison of two "planning" approaches dealing with temporal and/or discrete uncertainties and with a strong emphasis on robust execution. The first approach is based on chronicles and constraint satisfaction techniques; it relies on a causal link partial order temporal planner, in our case IxTeT. The second approach is based on timed game automata and reachability analysis, and uses the UPPAAL-TIGA system. The comparison is both qualitative (the kind of problems modeled and the properties of plans obtained) and quantitative (experimental results on a real example). To make this comparison possible, we propose a general scheme to translate a subset of IxTeT planning problems into UPPAAL-TIGA game-reachability problems. A direct consequence of this automated process would be the possibility to apply validation and verification techniques available in the timed automata community.

Details

TCS Journal 2006 Journal Article

Scheduling with timed automata

Yasmina Abdeddaı¨m
Eugene Asarin
Oded Maler

In this work, we present timed automata as a natural tool for posing and solving scheduling problems. We show how efficient shortest path algorithms for timed automata can find optimal schedules for the classical job-shop problem. We then extend these results to synthesize adaptive scheduling strategies for problems with uncertainty in task durations.

Details DOI

TCS Journal 1995 Journal Article

Reachability analysis of dynamical systems having piecewise-constant derivatives

Eugene Asarin
Oded Maler
Amir Pnueli

In this paper we consider a class of hybrid systems, namely dynamical systems with piecewise-constant derivatives (PCD systems). Such systems consist of a partition of the Euclidean space into a finite set of polyhedral sets (regions). Within each region the dynamics is defined by a constant vector field, hence discrete transitions occur only on the boundaries between regions where the trajectories change their direction. With respect to such systems we investigate the reachability question: Given an effective description of the systems and of two polyhedral subsets P and Q of the state-space, is there a trajectory starting at some xϵP and reaching some point in Q? Our main results are a decision procedure for two-dimensional systems, and an undecidability result for three or more dimensions.

Details DOI