  The analysis of complex dynamic systems is a core research topic in formal
methods and AI, and combined modelling of systems with data has gained
increasing importance in applications such as business process management. In
addition, process mining techniques are nowadays used to automatically mine
process models from event data, often without correctness guarantees. Thus
verification techniques for linear and branching time properties are needed to
ensure desired behavior. Here we consider data-aware dynamic systems with
arithmetic (DDSAs), which constitute a concise but expressive formalism of
transition systems with linear arithmetic guards. We present a CTL* model
checking procedure for DDSAs that relies on a finite-state abstraction by means
of a set of formulas that capture variable configurations. Linear-time
verification was shown to be decidable in specific classes of DDSAs where the
constraint language or the control flow are suitably confined. We investigate
several of these restrictions for the case of CTL*, with both positive and
negative results: CTL* verification is proven decidable for monotonicity and
integer periodicity constraint systems, but undecidable for feedback free and
bounded lookback systems. To demonstrate the feasibility of our approach, we
implemented it in the SMT-based prototype ada, showing that many practical
business process models can be effectively analyzed.
