@article{FraenzleHansen:BranchingTimeDCJournal,
  author =       {Martin Fr{\"a}nzle and Hansen, Michael R.},
  title =        {Efficient Model Checking for Duration Calculus},
  journal =      {International Journal of Software and Informatics},
  volume = "3",
  number = "2--3",
  pages = "171--196",
  year =         {2009},
  subproject = {R1},
  access = {restricted},
  bibtex = {fraenzle.ijsi09.bib},
  pdf = {fraenzle.ijsi09.pdf},
  abstract={Duration Calculus (abbreviated to DC) is an interval-based, 
            metric-time temporal logic designed for reasoning about embedded 
            real-time systems at a high level of abstraction. But the 
            complexity of model checking any decidable fragment featuring 
            both negation and chop, DC’s only modality, is non-elementary 
            and thus impractical. Even worse, when such decidable fragments 
            are generalized just slightly to cover more interesting durational 
            constraints the resulting fragments become undecidable. We here 
            investigate a similar approximation as frequently employed in 
            model checking situation- or point-based temporal logics, where 
            linear-time problems are safely approximated by branching-time 
            counterparts amenable to more efficient model-checking algorithms. 
            Mimicking the role that a situation has in (A)CTL as the origin 
            of a set of linear traces, we define a branching-time counterpart 
            to interval-based temporal logics building on situation pairs 
            spanning sets of intervals. While this branching-time interval 
            semantics yields the desired reduction in complexity of the 
            model-checking problem, from undecidable to linear in the size 
            of the formula and cubic in the size of the model, the 
            approximation is too coarse to be practical. We therefore refine 
            the semantics by an occurrence count for crucial states (e.g., 
            cuts of loops) in the model, arriving at a 4-fold exponential 
            model-checking problem sufficiently accurately approximating 
            the original one. Furthermore, when chop occurs in negative 
            polarity only in DC formulas, we have a doubly exponential 
            model-checking algorithm.},
}