Name
Abstract | ||
|---|---|---|
In the quantitative verification and synthesis of reactive systems, the states or transitions of a system are associated with payoffs, and a quantitative property of a behavior of the system is often characterized by the mean payoff for the behavior. This paper proposes an extension of LTL thatdescribes mean-payoff constraints. For each step of a behavior of a system, the payment depends on a system transition and a temporal property of the behavior. A mean-payoff constraint is a threshold condition for the limit supremum or limit infimum of the mean payoffs of a behavior. This extension allows us to describe specifications reflecting qualitative and quantitative requirements on long-run average of costs and the frequencies of satisfaction of temporal properties. Moreover, we develop an algorithm for the emptiness problems of multi-dimensional payoff automata with Büchi acceptance conditions and multi-threshold mean-payoff acceptance conditions. The emptiness problems are decided by solving linear constraint satisfaction problems, and the decision problems of our logic are reduced to the emptiness problems. Consequently, we obtain exponential-time algorithms for the model- and satisfiability-checking of the logic. Some optimization problems of the logic can also be reduced to linear programming problems. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-34281-3_19 | ICFEM |
Keywords | Field | DocType |
temporal logic,multi-threshold mean-payoff acceptance condition,reactive system,emptiness problem,temporal property,mean payoff,mean-payoff constraint,ltl thatdescribes mean-payoff constraint,quantitative requirement,quantitative property,system transition,linear programming,automata,decision problems,formal verification | Mathematical optimization,Decision problem,Computer science,Theoretical computer science,Linear temporal logic,Constraint satisfaction problem,Linear programming,Temporal logic,Optimization problem,Stochastic game,Formal verification | Conference |
Citations | PageRank | References |
10 | 0.57 | 18 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Takashi Tomita | 1 | 10 | 0.91 |
| Shin Hiura | 2 | 10 | 0.57 |
| Shigeki Hagihara | 3 | 78 | 12.33 |
| Naoki Yonezaki | 4 | 107 | 20.02 |