Record Details

Model-Checking in Presburger Counter Systems using Accelerations

Electronic Theses of Indian Institute of Science

View Archive Info
 
 
Field Value
 
Title Model-Checking in Presburger Counter Systems using Accelerations
 
Creator Acharya, Aravind N
 
Subject Computer Systems - Testing and Measurement
Presburger Counter Systems
Presburger Arithmetic
Model Checking
Presburger Counter Systems - Model Checking
Computational Tree Logic (CTL)
Generic Algorithms
Infinite State Counter Systems - Verification
Model Checking Algorithms
Counter Systems
Acceleration (Counter Systems)
Automated Verification
Computer Science
 
Description 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.
 
Contributor Raghavan, K V
 
Date 2018-04-18T06:46:54Z
2018-04-18T06:46:54Z
2018-04-18
2013
 
Type Thesis
 
Identifier http://etd.iisc.ernet.in/2005/3420
http://etd.iisc.ernet.in/abstracts/4287/G25923-Abs.pdf
 
Language en_US
 
Relation G25923