Skip to content

MultiQuaTEx

Jump to bottom
Andrea Vandin edited this page Feb 16, 2026 · 1 revision

MultiVeStA has a proprietary query language to express properties of interest. Here we provide information on it.

See, e.g., this paper, for an overview

MultiQuaTEx is a practitioner-oriented query language, or quantitative logic, to express quantitative temporal formulas. See the paper above for references about a discussion on the relation among the transient fragments of MultiQuaTEx, CSL, and PCTL.

Transient analysis

This is an example of query for transient analysis from the above paper

1: ObsAtStep(step,obs) =
2: if ( s.rval("steps") == step )
3: then s.rval(obs)
4: else next(ObsAtStep(step,obs)) fi ;
5: eval parametric(E[ ObsAtStep(x,"avg_distance_from_centroid")],E[ MyProperty(x,"avg_visible_neighbors")],x,1,5,601);

Lines 1-4 specify a recursive temporal operator ObsAtStep(step,obs), while line 5 specifies that the steps to consider are all from 1 to 601, with increment 5 (120 steps of interest overall). Instead, the two observations obs to be studied in these steps are avg_distance_from_centroid and avg_visible_neighbors discussed in the paper above. % Line 5 instructs MultiVeStA to evaluate the expected value of several instances of the temporal operator.

The temporal operator will be unrolled for each of the 120 steps of interest and for the two observations, (ObsAtStep(1,obs), ..., ObsAtStep(601,obs)), leading to 240 independent estimations. Each instance will undergo the shown recursive if-then-else computation: whenever the simulation is in the corresponding step, s.rval(obs) will trigger the execution of method eval in the code connecting MultiVeStA with the simulator at hand, otherwise the next in line 4 will trigger the execution of one step of simulation (method next), and the operator will be re-evaluated in the obtained simulation state.

  • This is one of the most common temporal operators defined in MultiQuaTEx.

We ask MultiVeStA to estimate each of these 240 expected values with 95% confidence intervals (CIs) of width at most 1. At the same time, we impose a maximum number of simulations (600). MultiVeStA will keep performing rounds of 30 simulations, each time evaluating the estimates and CIs. As soon as the CI of an estimate gets smaller than 1, it is not considered anymore. MultiVeStA completes its analysis as soon as all estimates reach the required CI width, or upon performing 600 simulations (possibly returning a CIs larger than 1). Clearly, each of the 240 estimations might require a different number of simulations, and in some cases 600 simulations might not be enough to bound the CI width to 1. % The choice of setting $\delta=1$ and maximum number of simulations 600 has been made arbitrarily for the sake of presentation. In practice, this could be tuned as follow: one could impose a smaller $\delta$, no limit on the number of simulations, and ask MultiVeStA to produce CSV files with estimations and CI widths computed after every round of 30 simulations. Then, one could either wait for all 240 estimations to reach the required CI width, or terminate the analysis when the latter round or simulations gave satisfactory CI widths.

Steady state analysis

Queries for steady-state analysis are typically much simpler, as we do not have to encode the recursive iterations presented above.

This are two examples of queries for steady state analysis from the above paper

1: Obs(obs) = s.rval(obs)
2: eval autoRD(E[ ObsAtStep("ratioHappy")]);
3:
4: Obs(obs) = s.rval(obs)
5: eval autoBM(E[ ObsAtStep("ratioHappy")]);

Our goal in the above paper was to confirm that the Schelling model, and in particular the ratio of happy agents, stabilizes over time. We did this using the steady-state analysis capabilities of MultiVeStA. We used these two MultiQuaTEx queries. For the first query, MultiVeStA runs autoRD. For the second, MultiVeStA runs autoBM. See this paper for details on the two algorithms

Please navigate the wiki using the right-menu

Clone this wiki locally