# Monitoring Traces for Satisfaction of Temporal Logic Properties

I am trying to implement a monitor for a certain temporal logic. What this means is the following:

• There is some external source, from which a trace of items are coming. An item looks like a timestamp along with some propositions which holds at that point.
• There is a property of traces we care about. This is specified in some temporal logic. This could look like "So far, p has been true" or "Since q happened in the last two time units, r has always held since then", or "p always holds when q does"
• Our task is to build a monitor which is a streaming algorithm whose interface is the operation step which consumes an item from the trace and checks whether the trace fed so far satisfies the given property or not.

import Control.Monad.State
import qualified Data.Map
import qualified Data.Set
import Data.Maybe

-- in what follows, t stands for some time domain. For most purposes, we assume it is totally ordered and has subtraction defined on it.

data Interval t =
OpenOpen t t
| OpenClosed t t
| ClosedOpen t t
| ClosedClosed t t
deriving (Eq, Ord)

inInterval :: Ord t => t -> Interval t -> Bool
inInterval t (OpenOpen       s f) = s < t && t < f
inInterval t (OpenClosed     s f) = s < t && t <= f
inInterval t (ClosedOpen     s f) = s <= t && t < f
inInterval t (ClosedClosed   s f) = s <= t && t <= f

inleqInterval :: Ord t => t -> Interval t -> Bool
inleqInterval t (OpenOpen       s f) = t < f
inleqInterval t (OpenClosed     s f) = t <= f
inleqInterval t (ClosedOpen     s f) = t < f
inleqInterval t (ClosedClosed   s f) = t <= f

-- Below, we use prop to denote a domain for the symbols that represent propositions
-- For most purposes, we'd want to use something like int since we'd use formulae based on this symbols as indices of maps

type TruthAssignment prop = Data.Set.Set prop
type Item t prop = (t, TruthAssignment prop)
type Trace t prop = [Item t prop] -- the programmer should ensure that the timestamps are increasing

data TemporalFormula t prop =
Proposition prop
| Since (Interval t) (TemporalFormula t prop) (TemporalFormula t prop)
| Neg (TemporalFormula t prop)
| And (TemporalFormula t prop) (TemporalFormula t prop)
deriving (Eq, Ord)

isTemporal :: TemporalFormula t prop -> Bool
isTemporal (Since _ _ _) = True
isTemporal _ = False

getTemporalSubformulas :: TemporalFormula t prop -> [TemporalFormula t prop]
getTemporalSubformulas phi@(Since _ phi1 phi2) = [phi] ++ getTemporalSubformulas phi1 ++ getTemporalSubformulas phi2
getTemporalSubformulas (Neg phi)                 = getTemporalSubformulas phi
getTemporalSubformulas (And phi1 phi2)           = (getTemporalSubformulas phi1) ++ (getTemporalSubformulas phi2)
getTemporalSubformulas _                         = []

type MonitorState t prop = Data.Map.Map (TemporalFormula t prop) [t]

-- the following type signature says that the monitor is a stateful object which when given a stream of items produces a stream of booleans
monitor :: (Ord t, Ord prop, Num t) => TemporalFormula t prop -> Trace t prop -> State (MonitorState t prop) [Bool]
monitor phi stream = do
iinit phi
loop stream
where
loop (i:is) = do
b <- step i phi
bs <- loop is
return (b:bs)
loop []     = return []

iinit :: (Ord t, Ord prop) => TemporalFormula t prop -> State (MonitorState t prop) ()
iinit phi = do
let subformulas = getTemporalSubformulas phi
put $foldr (\psi map -> Data.Map.insert psi [] map) Data.Map.empty subformulas step :: (Num t, Ord t, Ord prop) => Item t prop -> TemporalFormula t prop -> State (MonitorState t prop) Bool step (_, truths) (Proposition p) = return$ Data.Set.member p truths
step item (Neg formula) = not <$> step item formula step item (And formula1 formula2) = do b1 <- step item formula1 b2 <- step item formula2 return$ b1 && b2
step item@(tao, _) phi@(Since inter phi1 phi2) = do
update item phi
bufffs <- get
let lphi = case (Data.Map.lookup phi bufffs) of Just l -> l
case lphi of
[]    -> return False
(t:_) -> return $inInterval (tao - t) inter update :: (Num t, Ord t, Ord prop) => Item t prop -> TemporalFormula t prop -> State (MonitorState t prop) () update (time, truths) phi@(Since inter phi1 phi2) = do bufffs <- get let lphi = case (Data.Map.lookup phi bufffs) of Just l -> l b1 <- step (time, truths) phi1 b2 <- step (time, truths) phi2 let l = if b1 then (ddrop lphi inter time) else [] let lphi' = if b2 then l ++ [time] else l put (Data.Map.insert phi lphi' bufffs) ddrop :: (Ord t, Num t) => [t] -> Interval t -> t -> [t] ddrop [] _ _ = [] ddrop (kappa:ls) inter tao | inleqInterval (tao - kappa) inter = ddrop' kappa ls inter tao | otherwise = ddrop ls inter tao ddrop' :: (Ord t, Num t) => t -> [t] -> Interval t -> t -> [t] ddrop' kappa [] _ _ = [kappa] ddrop' kappa (kappa':ls) inter tao | inInterval (tao - kappa') inter = ddrop' kappa' ls inter tao | otherwise = (kappa:kappa':ls)  For comparison, here is a Java implementation of the same idea. I would like some feedback on my Haskell code: • I would like to be able to extend this code with a main and test it on a large stream to see how well it performs. Is the State Monad appropriate for the purpose of performance? Is my way of modelling streams as lists appropriate for this purpose? • As implemented, the "monitor state" and the Formula looks like independent objects. Is there a better way to tie them together than to define a seperate MonitorState and initalize it everytime? I think the idea of modelling MonitorState as a Map is ugly and not very haskell-y. What are some better ways of structuring my code so that I can avoid the Map and/or show that there is some relation between the state of the monitor and a formula? • Other general comments on improving the code quality. ## 1 Answer I can't comment on performance implications of state monad usage, but it seems like list concatenation may be a bottleneck (e.g. in getTemporalSubformulas or l ++ [time] in update). Minor style notes It is common practice to import Data.Map and Data.Set with alias and to import main type unqualified. This makes type signatures a bit more concise. import qualified Data.Map as Map import Data.Map (Map) foo :: Int -> Map Int String foo x = Map.singleton x "hello"  In isTemporal you can use {} to match on data constructor without matching its fields. This is potentially future-proof in case of changing number of fields in data constructor. isTemporal Since{} = True isTemporal _ = False  It may be a bit easier to encode intervals as a pair of bounds: data EndPoint t = Open t | Closed t type Interval t = (EndPoint t, EndPoint t) afterStart, beforeEnd :: Ord t => t -> Interval t -> Bool afterStart t (Open start) = t > start afterStart t (Closed start) = t >= start beforeEnd t (Open end) = t < end beforeEnd t (Closed end) = t <= end inInterval, inleqInterval :: Ord t => t -> Interval t -> Bool inInterval t int = afterStart t int && beforeEnd t int inleqInterval = beforeEnd  It is also may be beneficial to reuse intervals from data-interval package. In iinint foldr (\psi map -> Data.Map.insert psi [] map) Data.Map.empty subformulas  can be rewritten as Map.fromList$ map (,[]) subformulas


Try to compile with -Wall flag, seems like you have a lot of non-exhaustive pattern matches, which is bad.

For example:

  let lphi = case (Data.Map.lookup phi bufffs) of Just l -> l


If you are absolutely sure that lookup won't fail here, you can rewrite it with Data.Map.!:

  let lphi = bufffs Map.! phi


ddrop can be rewritten to make it more explicit what parts of the list you are removing:

ddrop ls inter tao = case dropWhile f ls of
[] -> []
kappa:ls' -> kappa : dropWhile g ls'
where
f kappa = not $inleqInterval (tao - kappa) inter g kappa = inInterval (tao - kappa) inter  or a bit shorter with the ViewPatterns extension ddrop ls inter tao = case dropWhile f ls of | dropWhile f ls -> kappa:ls' = kappa : dropWhile g ls' | otherwise = [] where f kappa = not$ inleqInterval (tao - kappa) inter
g kappa = inInterval (tao - kappa) inter