Specification languages for stutter-invariant regular properties. (English) Zbl 1262.68114
Liu, Zhiming (ed.) et al., Automated technology for verification and analysis. 7th international symposium, ATVA 2009, Macao, China, October 14–16, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04760-2/pbk). Lecture Notes in Computer Science 5799, 244-254 (2009).
Summary: We present specification languages that naturally capture exactly the regular and \(\omega \)-regular properties that are stutter invariant. Our specification languages are variants of the classical regular expressions and of the core of PSL, a temporal logic, which is widely used in industry and which extends the classical linear-time temporal logic LTL by semi-extended regular expressions.
For the entire collection see [Zbl 1176.68012].
For the entire collection see [Zbl 1176.68012].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
References:
| [1] | IEEE standard for property specification language (PSL). IEEE Std 1850TM (October 2005) |
| [2] | Alur, R.; Brayton, R. K.; Henzinger, T. A.; Qadeer, S.; Rajamani, S. K., Partial-order reduction in symbolic state-space exploration, Form. Method. Syst. Des., 18, 2, 97-116 (2001) · Zbl 1001.68080 · doi:10.1023/A:1008767206905 |
| [3] | Beer, I.; Ben-David, S.; Eisner, C.; Geist, D.; Gluhovsky, L.; Heyman, T.; Landver, A.; Paanah, P.; Rodeh, Y.; Ronin, G.; Wolfsthal, Y.; Marie, R.; Plateau, B.; Calzarossa, M. C.; Rubino, G. J., RuleBase: Model checking at IBM, Computer Performance Evaluation Modelling Techniques and Tools, 480-483 (1997), Heidelberg: Springer, Heidelberg |
| [4] | Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL. Technical report, The Prosyd Project (2005), http://www.prosyd.org |
| [5] | Bustan, D.; Havlicek, J.; Ball, T.; Jones, R. B., Some complexity results for SystemVerilog assertions, Computer Aided Verification, 205-218 (2006), Heidelberg: Springer, Heidelberg · Zbl 1188.68184 · doi:10.1007/11817963_21 |
| [6] | Cimatti, A.; Roveri, M.; Tonetta, S., Symbolic compilation of PSL, IEEE Trans. on CAD of Integrated Circuits and Systems, 27, 10, 1737-1750 (2008) · doi:10.1109/TCAD.2008.2003303 |
| [7] | Dax, C., Klaedtke, F., Lange, M.: On regular temporal logics with past. In: Proceedings of the 36th International Colloquium on Automata, Languages, and Programming, ICALP (to appear, 2009) · Zbl 1248.68326 |
| [8] | Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering (ICSE), pp. 411-420 (1999), http://patterns.projects.cis.ksu.edu/ |
| [9] | Etessami, K.; Halbwachs, N.; Peled, D. A., Stutter-invariant languages, ω-automata, and temporal logic, Computer Aided Verification, 236-248 (1999), Heidelberg: Springer, Heidelberg · Zbl 1046.68591 · doi:10.1007/3-540-48683-6_22 |
| [10] | Etessami, K., A note on a question of Peled and Wilke regarding stutter-invariant LTL, Inform. Process. Lett., 75, 6, 261-263 (2000) · Zbl 1339.68166 · doi:10.1016/S0020-0190(00)00113-7 |
| [11] | Godefroid, P.; Wolper, P., A partial approach to model checking, Inf. Comput., 110, 2, 305-326 (1994) · Zbl 0806.68079 · doi:10.1006/inco.1994.1035 |
| [12] | Holzmann, G., Kupferman, O.: Not checking for closure under stuttering. In: Proceedings of the 2nd International Workshop on the SPIN Verification System. Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 163-169 (1996) · Zbl 0889.68102 |
| [13] | Lamport, L.: What good is temporal logic? In: Proceedings of the 9th IFIP World Computer Congress. Information Processing, vol. 83, pp. 657-668 (1983) |
| [14] | Lange, M.; Caires, L.; Vasconcelos, V. T., Linear time logics around PSL: Complexity, expressiveness, and a little bit of succinctness, CONCUR 2007 - Concurrency Theory, 90-104 (2007), Heidelberg: Springer, Heidelberg · Zbl 1151.68540 · doi:10.1007/978-3-540-74407-8_7 |
| [15] | Peled, D., Combining partial order reductions with on-the-fly model-checking, Form. Method. Syst. Des., 8, 1, 39-64 (1996) · Zbl 1425.68267 · doi:10.1007/BF00121262 |
| [16] | Peled, D.; Y. Vardi, M., Ten years of partial order reduction, Computer Aided Verification, 17-28 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0028727 |
| [17] | Peled, D.; Wilke, T., Stutter-invariant temporal properties are expressible without the next operator, Inform. Process. Lett., 63, 5, 243-246 (1997) · Zbl 1337.68170 · doi:10.1016/S0020-0190(97)00133-6 |
| [18] | Peled, D.; Wilke, T.; Wolper, P., An algorithmic approach for checking closure properties of temporal logic specifications and ω-regular languages, Theoret. Comput. Sci., 195, 2, 183-203 (1998) · Zbl 0915.68058 · doi:10.1016/S0304-3975(97)00219-3 |
| [19] | Rabinovich, A. M.; Brim, L.; Gruska, J.; Zlatuška, J., Expressive completeness of temporal logic of action, Mathematical Foundations of Computer Science 1998, 229-238 (1998), Heidelberg: Springer, Heidelberg · Zbl 0912.03011 · doi:10.1007/BFb0055772 |
| [20] | Valmari, A., A stubborn attack on state explosion, Form. Method. Syst. Des., 1, 4, 297-322 (1992) · Zbl 0783.68083 · doi:10.1007/BF00709154 |
| [21] | Vardi, M. Y.; Ramanujam, R.; Sarukkai, S., From philosophical to industrial logics, Logic and Its Applications, 89-115 (2009), Heidelberg: Springer, Heidelberg · Zbl 1209.68325 · doi:10.1007/978-3-540-92701-3_7 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
