An Implementation of Linear Temporal Logic for Driving Safety Suitable for the Concept of Local Dynamic Map

Author(s):  
Arvind Kumar ◽  
Hiroaki Wagatsuma
Electronics ◽  
2020 ◽  
Vol 9 (10) ◽  
pp. 1728
Author(s):  
Odilbek Urmonov ◽  
HyungWon Kim

To ensure the driving safety in vehicular network, it is necessary to construct a local dynamic map (LDM) for an extended range. Using the standard vehicular communication protocols, however, vehicles can construct the LDM for only one-hop range. Constructing large-scale LDM is highly challenging because vehicles randomly change their position. This paper proposes a dynamic map propagation (DMP) method, which builds a large aggregated LDM data using a multi-hop communication. To reduce the data overhead, we introduce an efficient clustering method based on a half-circle of the forwarder’s wireless range. The DMP elects one forwarder per cluster, which constructs LDM and forwards it to a neighbor cluster. The inter-cluster interference is minimized by allocating a different transmit window to each cluster. DMP copes with a dynamic environment by frequently re-electing the forwarders and their associated transmission windows. Simulation results reveal that DMP enhances the forwarders’ reception ratio by 20%, while extending LDM dissemination range by 29% over a previous work.


Automatica ◽  
2021 ◽  
Vol 130 ◽  
pp. 109723
Author(s):  
Sahar Mohajerani ◽  
Robi Malik ◽  
Andrew Wintenberg ◽  
Stéphane Lafortune ◽  
Necmiye Ozay

2020 ◽  
Vol 67 (6) ◽  
pp. 1-61
Author(s):  
Javier Esparza ◽  
Jan Křetínský ◽  
Salomon Sickert

2014 ◽  
Vol 513-517 ◽  
pp. 927-930
Author(s):  
Zhi Cheng Wen ◽  
Zhi Gang Chen

Object-Z, an extension to formal specification language Z, is good for describing large scale Object-Oriented software specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. Linear temporal logic can describe real-time system, but it can not deal with time variables well and also can not describe formal specification modularly. This paper extends linear temporal logic with clocks (LTLC) and presents an approach to adding linear temporal logic with clocks to Object-Z. Extended Object-Z with LTLC, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.


2002 ◽  
Vol 12 (6) ◽  
pp. 875-903 ◽  
Author(s):  
BART JACOBS

This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.


Sign in / Sign up

Export Citation Format

Share Document