# 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.