Hyperlink analysis using temporal logic

Abstract

Model Checking is an automatic technique for verifying finite state reactive systems. Specification is expressed using temporal logic and the system is specified as a state transition graph. I have utilized some Model checking techniques to alleviate some problems associated with browsing the internet that are collectively known as Cognitive Overload. Using Model checking techniques, the application that resented here is able to analyze a website using CTL formulae, as well as suggesting links and paths to follow through the website according to the users' criteria. Also, the application is able to dynamically hide or show certain sections of a website according to certain properties embedded into within the HTML.