Duration Calculus of Weakly Monotonic Time (WDC) is an
extension of DC to allow description of discrete processes where
several steps of computation can occur at the same time point. In
this paper, we introduce Linear Occurrence Invariants (LOI) which
is a subclass of WDC formulas and give an algorithm to check
real-time automata for LOI using integer programming. LOI can be
used effectively to specify system requirements in some cases
including when the system is considered under the true synchrony
assumption. We also extend WDC probabilistically to express
dependability requirements of real-time systems and develop
techniques to check deterministic probabilistic real-time automata
for a class of probabilistic WDC formulas.