Parameterized model checking is the problem of deciding if a given formula holds irrespective of the number of participating processes. A standard approach for solving the parameterized model checking problem is to reduce it to model checking finitely many finite-state systems. This work considers the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases where model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Büchi word automaton), and establish tight bounds on the sizes of such automata.

This paper contributes to a sustainable construction design management approach to increase the successful renovation rate of existing residential building stock. Indeed, coupling BIM with mixed reality can speed up and improve the quality of the renovation design processes, because it can display virtual models of alternative design scenarios superimposed over the existing physical facility. To this purpose, a sample of technicians was enrolled to test the reliability of this technology. A prototype was developed that enables cooperation among stakeholders and the implementation of an efficient workflow. The volunteers carried out real-life tests in a building demonstrator in Caceres (Spain) and filled in two questionnaires with their feedback. The results showed that an MR-based platform can involve interested stakeholders in the assessment of renovation design projects, that speeds up the decision-making process and increases the quality of those projects. Moreover, technicians can master the technology quickly, provided that it is included in the current renovation workflow and some technology gaps are covered. However, the main limitations of this study are that these findings are valid for building renovation design only, and the tests were performed in a controlled, yet full scale, experimental environment. Finally, this paper deals with a few open technical issues, such as the efficient alignment of holograms, transformation of BIM models into a format suitable for mixed reality applications and sharing feedbacks in an on-line repository to foster collaboration.