arXiv subjects

Edward A. Lee

Publications and source records attributed to Edward A. Lee.

22 records · Page 2Linked to original sources

arXiv2018

A Metric for Linear Temporal Logic

We propose a measure and a metric on the sets of infinite traces generated by a set of atomic propositions. To compute these quantities, we first map properties to subsets of the real numbers and then take the Lebesgue measure of the resulting sets. We analyze how this measure is computed for Linear Temporal Logic (LTL) formulas. An implementation for computing the measure of bounded LTL properties is provided and explained. This implementation leverages SAT model counting and effects independence checks on subexpressions to compute the measure and metric compositionally.

cs.LO↗

arXiv2016

Control Improvisation with Probabilistic Temporal Specifications

We consider the problem of generating randomized control sequences for complex networked systems typically actuated by human agents. Our approach leverages a concept known as control improvisation, which is based on a combination of data-driven learning and controller synthesis from formal specifications. We learn from existing data a generative model (for instance, an explicit-duration hidden Markov model, or EDHMM) and then supervise this model in order to guarantee that the generated sequences satisfy some desirable specifications given in Probabilistic Computation Tree Logic (PCTL). We present an implementation of our approach and apply it to the problem of mimicking the use of lighting appliances in a residential unit, with potential applications to home security and resource management. We present experimental results showing that our approach produces realistic control sequences, similar to recorded data based on human actuation, while satisfying suitable formal requirements.

eess.SY↗

arXiv2013

The Fixed-Point Theory of Strictly Contracting Functions on Generalized Ultrametric Semilattices

We introduce a new class of abstract structures, which we call generalized ultrametric semilattices, and in which the meet operation of the semilattice coexists with a generalized distance function in a tightly coordinated way. We prove a constructive fixed-point theorem for strictly contracting functions on directed-complete generalized ultrametric semilattices, and introduce a corresponding induction principle. We cite examples of application in the semantics of logic programming and timed computation, where, until now, the only tool available has been the non-constructive fixed-point theorem of Priess-Crampe and Ribenboim for strictly contracting functions on spherically complete generalized ultrametric semilattices.

cs.LO↗

arXiv2013

Numerical LTL Synthesis for Cyber-Physical Systems

Cyber-physical systems (CPS) are systems that interact with the physical world via sensors and actuators. In such a system, the reading of a sensor represents measures of a physical quantity, and sensor values are often reals ranged over bounded intervals. The implementation of control laws is based on nonlinear numerical computations over the received sensor values. Synthesizing controllers fulfilling features within CPS brings a huge challenge to the research community in formal methods, as most of the works in automatic controller synthesis (LTL synthesis) are restricted to specifications having a few discrete inputs within the Boolean domain. In this report, we present a novel approach that addresses the above challenge to synthesize controllers for CPS. Our core methodology, called numerical LTL synthesis, extends LTL synthesis by using inputs or outputs in real numbers and by allowing predicates of polynomial constraints to be defined within an LTL formula as specification. The synthesis algorithm is based on an interplay between an LTL synthesis engine which handles the pseudo-Boolean structure, together with a nonlinear constraint validity checker which tests the (in)feasibility of a (counter-)strategy. The methodology is integrated within the CPS research framework Ptolemy II via the development of an LTL synthesis module G4LTL and a validity checker JBernstein. Although we only target the theory of nonlinear real arithmetic, the use of pseudo-Boolean synthesis framework also allows an easy extension to embed a richer set of theories, making the technique applicable to a much broader audience.

cs.SE↗