Ruina/basural: Lógicas temporales y espaciales de la ciudad de La Paz en Saenz y Viscarra

This article analyzes spatio-temporal logics in the representation of the city of La Paz in Imágenes Paceñas by Jaime Saenz and the urban chronicles of Víctor Hugo Viscarra. Juxtaposing the concepts of chrononormativity and queer time, it explores how linear temporal logic remains insufficient for the understanding of the city and its inhabitants in the two narrative projects. The article postulates that the marginal spaces of architectural ruins and garbage dumps, and the marginalized people who inhabit queer space-time are key to “revealing the hidden city” and understanding its contradictory place in the national narrative and space.

LDES: Detector Design for Version Number Attack Detection using Linear Temporal Logic based on Discrete Event System

The Internet Engineering Task Force (IETF) has defined routing protocols for Low Power and Lossy Networks (RPL) for constrained devices. RPL constructs DODAGs (Destination Oriented Directed Acyclic Graphs), to optimize routing. RPL ensures acyclic topology with the DODAG version number. However, the control message's DODAG version number is not authenticated. So, RPL is vulnerable to topological inconsistency attack known as DODAG Version Number (DVN) attack. DVN attack creates a packet delay, packet loss, cyclic topology, etc., in the network. This paper proposes a method for detecting DODAG version number attacks. Several existing schemes to defend against the DVN, such as cryptographic techniques, trust-based, threshold-based and mitigation are computationally intensive or require protocol modification. DVN does not change the packet format or sequence of packets, but can still perform attacks and hence fall under the category of stealthy attacks, which are difficult to detect using traditional Intrusion Detection System$'$s (IDS). Discrete-Event System (DES) based IDS have been applied in the literature for stealthy attacks that achieve low overhead, low false alarm rate, etc. However, the construction of DES-based IDS for network protocol may lead to errors, as modelling is manual. The resulting IDS, therefore, is unable to guarantee its correctness. This paper proposes Linear Temporal Logic (LTL) based DES paradigm to detect DVN. LTL-based paradigm facilitates formal verification of the DES-based IDS, and hence the correctness of the scheme is ascertained. The proposed technique is simulated using the Contiki cooja simulator. When the percentage of spiteful nodes in the network increases, the true positive rate, and packet delivery rate drops, while the false positive rate and control message overhead increase. The memory requirement for sending the packets and verifying the nodes is minimal. The LTL-based IDS has been formally verified using NuSMV to ensure the correctness of the framework.

Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis

Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) assumption. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.

Synthesizing Good-Enough Strategies for LTLf Specifications

We consider the problem of synthesizing good-enough (GE)-strategies for linear temporal logic (LTL) over finite traces or LTLf for short. The problem of synthesizing GE-strategies for an LTL formula φ over infinite traces reduces to the problem of synthesizing winning strategies for the formula (∃Oφ)⇒φ where O is the set of propositions controlled by the system. We first prove that this reduction does not work for LTLf formulas. Then we show how to synthesize GE-strategies for LTLf formulas via the Good-Enough (GE)-synthesis of LTL formulas. Unfortunately, this requires to construct deterministic parity automata on infinite words, which is computationally expensive. We then show how to synthesize GE-strategies for LTLf formulas by a reduction to solving games played on deterministic Büchi automata, based on an easier construction of deterministic automata on finite words. We show empirically that our specialized synthesis algorithm for GE-strategies outperforms the algorithms going through GE-synthesis of LTL formulas by orders of magnitude.