Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Combining Forward And Backward Analyses of Temporal Properties

Damien MasséContact Information

(5)  LIX, École Polytechnique, Palaiseau, France
Abstract
In this paper we extend the well-known combination of forward and backward static analyses in abstract interpretation for the verification of complex temporal properties for transition systems. First, we show that this combination, whose results are often better than those obtained by using both analyses separately, can be used to check simple temporal properties with just one fixpoint. Then we extend this result to more complex temporal properties, including a superset of Ctl in the case of non-game properties, and a superset of Atl in the case of game properties.

Contact Information Damien Massé
Email: masse@lix.polytechnique.fr
URL: http://www.lix.polytechnique.fr/~masse/
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.81 • Server: mpweb05
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)