Verification of Properties of Human-Computer Dialogues with an Infinite Number of States

One of the advantages of using formal methods in human-computer interfaces is the possibility to reason about user interface properties. Model checking techniques provide a useful support for this purpose. This paper discusses the problem of verifying the properties of user interfaces when the dialogue specification has an infinite number of states. Recent techniques allow designers to get some results even in this particular case and we discuss when such results are useful for verifying the user interface properties.