China
Africa
Explore chapters and articles related to this topic
Temporal Logic Motion Planning in Robotics
Published in Jitendra R. Raol, Ajith K. Gopal, Mobile Intelligent Autonomous Systems, 2016
Temporal rover (TR) [19] is a specification-based commercial tool for programmes written in C, C++, Java, Verilog and VHDL. In TR, the user annotates the sections of the target programme where a property needs to be checked at runtime. TR supports the following formalisms: linear-time temporal logic (LTL) and metric temporal logic (MTL) and the properties which can be specified with these logics include future time temporal properties as well as lower and upper bound properties, and relative-time and real-time properties. The tool takes the target programme as its input and its parser generates an identical programme to the properties inserted in the target programme, and during execution the generated code validates the executing programme against specified properties.
Metric dynamic equilibrium logic
Published in Journal of Applied Non-Classical Logics, 2023
Arvid Becker, Pedro Cabalar, Martín Diéguez, Luis Farinas del Cerro, Torsten Schaub, Anna Schuhmann
In Cabalar et al. (2022), we filled this gap in the context of temporal logic by associating each state with its time, as done in Metric Temporal Logic (MTL (Koymans, 1990)). This resulted in a non-monotonic metric temporal extension of HT, referred to as MEL. It allows us to measure time differences between events. For instance, in our example, we may thus express that whenever the machine is used, it has to be cleaned within 60 to 120 time units, by writing: Unlike the non-metric version, this stipulates that once is true in a state, must be true in some future state whose associated time is at least 60 and at most 120 time units after the time of . The choice of time domain is crucial, and might even lead to undecidability in the continuous case (that is, using real numbers). We rather adapt a discrete approach that offers a sequence of snapshots of a dynamic system.