LTL Pattern Formulas

We give some example LTL properties which can be specified in IscasMC. In our tool, such formulas can be used in form form \ltlP(\ldots) for Markov chains and as \ltlPmax(\ldots) or \ltlPmin(\ldots) for Markov decision processes, where \ldots denotes the formula under consideration.

  • Bounded responsibility property, \bigwedge_i \ltlG \, \mathrm{req}_i \rightarrow \ltlF^{\leq \mathrm{bound}} \, \mathrm{reply}_i: for a family of components, each component i replies to a given request within a given time bound.
  • Bounded responsibility property with fairness, \bigwedge_i \ltlG \ltlF \, \mathrm{req}_i \wedge \bigwedge_i \ltlG \, \mathrm{req}_i \rightarrow \ltlF^{\leq \mathrm{bound}} \, \mathrm{reply}_i: similar to bounded responsibility, suitable for \ltlPmax in MDPs. The fairness ensures that the system is scheduled such that the request occurs infinitely often.
  • Bounded responsibility property with fairness, \bigwedge_i \ltlG \ltlF \, \mathrm{req}_i \rightarrow \left(\bigwedge_i \ltlG \, \mathrm{req}_i \rightarrow \ltlF^{\leq \mathrm{bound}} \, \mathrm{reply}_i\right): similar to bounded responsibility, suitable for \ltlPmin in MDPs. The fairness ensures that the system is scheduled such that the request occurs infinitely often.