Model-Checking in Presburger Counter Systems using Accelerations
Acharya, Aravind N
MetadataShow full item record
Model checking is a powerful technique for analyzing reach ability and temporal properties of finite state systems. Model-checking finite state systems has been well-studied and there are well known efficient algorithms for this problem. However these algorithms may not terminate when applied directly to in finite state systems. Counter systems are a class of in fininite state systems where the domain of counter values is possibly in finite. Many practical systems like cache coherence protocols, broadcast protocols etc, can naturally be modeled as counter systems. In this thesis we identify a class of counter systems, and propose a new technique to check whether a system from this class satires’ a given CTL formula. The key novelty of our approach is a way to use existing reach ability analysis techniques to answer both \until" and \global" properties; also our technique for \global" properties is different from previous techniques that work on other classes of counter systems, as well as other classes of in finite state systems. We also provide some results by applying our approach to several natural examples, which illustrates the scope of our approach.
Showing items related by title, author, creator and subject.
Paul, Geeta Kheter (2011-05-26)
Sai Keerthi T, DivyaThe open medium, dynamic topology and distributed operation in Mobile Ad hoc Networks (MANET) leads to high risks. Many solutions are proposed to protect a MANET from attacks, ranging from attack identification to ...
A Theoretical Model And Empirical Analysis Of Components Of Spread In Over The Counter Exchange Of India Rao, Jyothi G (Indian Institute of Science, 2007-03-26)Over the Counter Exchange of India (OTCEI) was established in 1992 mainly to provide a platform for small and medium sized companies to raise money for their capital requirements. It is a well defined dealer market with ...