Show simple item record

dc.contributor.advisorRaghavan, K V
dc.contributor.authorKommineni, Vasanta Lakshmi
dc.date.accessioned2020-04-29T07:52:46Z
dc.date.available2020-04-29T07:52:46Z
dc.date.submitted2018
dc.identifier.urihttps://etd.iisc.ac.in/handle/2005/4388
dc.description.abstractCounter systems are a well-known and powerful modeling notation for specifying infnite state systems. In this thesis we target the problem of checking temporal properties of counter systems. We address three predominant families of temporal property specifications, namely Computation Tree Logics (CTL and CTL*) and Linear Temporal Logic (LTL). We provide two novel techniques to model check LTL and CTL properties of counter systems. We then provide a third technique to model check CTL temporal properties, which uses our LTL model checking technique as a sub-routine and is a modified version of an existing technique for finite-state systems. Each of our techniques returns a Presburger formula, which encodes the set of reachable states of the given system that satisfy the given temporal property. A novel aspect of our techniques is that they perform iterative analysis using reachability analysis sub-routines of counter systems. This brings two advantages to the table. The first is that these algorithms are able to compute precise answers on a much wider class of systems than previous approaches. Secondly, they compute results by iterative expansion or contraction, and hence permit an over-approximated or under- approximated solution to be obtained at any point even in cases where termination may not occur.For each of the three techniques we propose in this thesis, we formally prove its correctness, and also give a theoretical characterization of the class of counter systems for which it can terminate with precise results. We also provide an implementation of our CTL and LTL model checking techniques. We present experimental results on standard benchmarks (such as cache coherence protocols, communication protocols, control mechanisms etc. modeled as counter systems), which demonstrate the precision as well as efficiency of our techniques.en_US
dc.language.isoen_USen_US
dc.relation.ispartofseries;G28713
dc.rightsI grant Indian Institute of Science the right to archive and to make available my thesis or dissertation in whole or in part in all forms of media, now hereafter known. I retain all proprietary rights, such as patent rights. I also retain the right to use in future works (such as articles or books) all or part of this thesis or dissertationen_US
dc.subjectComputation Tree Logicsen_US
dc.subjectLinear Temporal Logicen_US
dc.subject.classificationResearch Subject Categories::TECHNOLOGY::Information technology::Computer science::Computer scienceen_US
dc.titleModel Checking Temporal Properties of Presburger Counter Systemsen_US
dc.typeThesisen_US
dc.degree.namePhDen_US
dc.degree.levelDoctoralen_US
dc.degree.grantorIndian Institute of Scienceen_US
dc.degree.disciplineEngineeringen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record