A Past-Linear Temporal Logic (PLTL) property for a sender/receiver model taken from Bounded Verification of Past LTL:
G (sender.state = waitForAck => Y (H sender.state != waitForAck))
which states that, it Globally holds that if the sender is waitingForAck, then Yesterday (i.e. at the previous instant), Historically it held that the sender state was not waitingForAck. In other words, the sender waits for acknowledgement at most once during the execution.
The only input stream is the state of the sender at each instant.
The only output stream is the value of the property at each instant.
A Metric Temporal Logic (MTL) property to establish deadlines between environment events and the corresponding system responses taken from Some Recent Results in Metric Temporal Logic:
G (alarm => (F[0,10] allclear || F[10,10] shutdown))
The property assesses that an alarm is followed by a shutdown event in exactly 10 time units unless all clear is sounded first.
The only input stream is the event happening at each instant.
The only output stream is the value of the property at each instant.
TradingView is an online charting platform for stock exchange, which offers a series-oriented language to create customized studies and signals (called Pinescript) and run them in the company servers.
We have implemented the indicators of Pinescript in HLola as a library, and we show the implementation of a trading strategy using the HLola Pinescript library.
The input streams are the close and high values of a stock at each day.
The output streams indicate how much stock to buy or sell every day.
The input streams of this specification consist of the state of the UAV at every instant and the onboard camera events to detect when a picture is being captured.
The output streams are the values of properties 1. and 2.
This specification estimates the trajectory of a flying UAV to assess if it will reach its target destination.
The input streams are data on the state of the vehicle at every instant and its target destination.
The output stream shows how close to the target destination will the vehicle fly.
This specification is ECG.
The input streams of this specification consist of the timestamp and the measurement.
The output streams are the timestamp and if it is a peak.