Search

International audience

The use of smart homes has been increasing greatly in recent years thanks to considerable achievements in technology. Home automation aims to improve person's autonomy and safety. For that reason, many indoor localization systems were developed recently. Nevertheless, their efficiency were improved for a single inhabitant and can not be applied in the presence of an outsider. For this purpose, the aim of this work is to design a wireless sensors network and develop a novel approach which can track multiple humans in an indoor environment. The proposed method uses a satisfiability (SAT) checker for boolean combinations of arithmetic constraints over real- and integer-valued variables. This algorithm is implemented in a set-membership framework dealing with faulty measurements. An illustrative example and experimental results are provided throughout this paper to show the performance of our method.

International audience; Aiming at automatic verification and analysis techniques for hybrid discrete-continuous systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art interval solver for ODEs, and with bracketing systems, which exploit monotonicity properties allowing to find enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply the combined iSAT-ODE solver to the analysis of a variety of non-linear hybrid systems by solving predicative encodings of reachability properties and of an inductive stability argument, and evaluate the impact of the different enclosure methods, decision heuristics, and their combination. Our experiments include classic benchmarks from the literature, as well as a newly-designed conveyor belt system that combines hybrid behavior of parallel components, a slip-stick friction model with non-linear dynamics and flow invariants, and several dimensions of parameterization. In the paper, we also present and evaluate an extension of VNODE-LP tailored to its use as a deduction mechanism within iSAT-ODE, to allow fast re-evaluations of enclosures over arbitrary subranges of the analyzed time span.

International audience; Aiming at automatic verification and analysis techniques for hybrid systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our pre- vious work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art enclosure method for ODEs, and with bracketing systems which exploit monotonicity properties to find enclo- sures for problems that VNODE-LP alone cannot enclose tightly. We apply our method to the analysis of a non-linear hybrid system by solv- ing predicative encodings of an inductive stability argument and evaluate the impact of different methods and their combination.

International audience; We study the reactive synthesis problem (RS) for specifications given in Metric Interval Temporal Logic (MITL). RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D'Souza et al. and Bouyer et al.). In this paper, we precise the decidabil-ity border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it.