On error estimation for reduced-order modeling of linear non-parametric and parametric systems

Motivated by a recently proposed error estimator for the transfer function of the reduced-order model of a given linear dynamical system, we further develop more theoretical results in this work. Moreover, we propose several variants of the error estimator, and compare those variants with the existing ones both theoretically and numerically. It is shown that some of the proposed error estimators perform better than or equally well as the existing ones. All the error estimators considered can be easily extended to estimate the output error of reduced-order modeling for steady linear parametric systems.

METHODS OF OPTIMIZATION OF PARAMETRIC SYSTEMS

The paper considers methods of parametric optimization of a dynamical system, which is described by a parametric system of differential equations. The gradient of the functional in the form of Boltz is found, which is the basis of methods such as gradient descent. Another method is based on the application of the sensitivity function.

Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning

The problem of invariant checking in parametric systems – which are required to operate correctly regardless of the number and connections of their components – is gaining increasing importance in various sectors, such as communication protocols and control software. Such systems are typically modeled using quantified formulae, describing the behaviour of an unbounded number of (identical) components, and their automatic verification often relies on the use of decidable fragments of first-order logic in order to effectively deal with the challenges of quantified reasoning.In this paper, we propose a fully automatic technique for invariant checking of parametric systems which does not rely on quantified reasoning. Parametric systems are modeled with array-based transition systems, and our method iteratively constructs a quantifier-free abstraction by analyzing, with SMT-based invariant checking algorithms for non-parametric systems, increasingly-larger finite instances of the parametric system. Depending on the verification result in the concrete instance, the abstraction is automatically refined by leveraging canditate lemmas from inductive invariants, or by discarding previously computed lemmas.We implemented the method using a quantifier-free SMT-based IC3 as underlying verification engine. Our experimental evaluation demonstrates that the approach is competitive with the state of the art, solving several benchmarks that are out of reach for other tools.

Visuo-Locomotive Complexity as a Component of Parametric Systems for Architecture Design

A people-centred approach for designing large-scale built-up spaces necessitates systematic anticipation of user’s embodied visuo-locomotive experience from the viewpoint of human-environment interaction factors pertaining to aspects such as navigation, wayfinding, usability. In this context, we develop a behaviour-based visuo-locomotive complexity model that functions as a key correlate of cognitive performance vis-a-vis internal navigation in built-up spaces. We also demonstrate the model’s implementation and application as a parametric tool for the identification and manipulation of the architectural morphology along a navigation path as per the parameters of the proposed visuospatial complexity model. We present examples based on an empirical study in two healthcare buildings, and showcase the manner in which a dynamic and interactive parametric (complexity) model can promote behaviour-based decision making throughout the design process to maintain desired levels of visuospatial complexity as part of a navigation or wayfinding experience.