A model is studied in the full range of all operational parameters of the unsteady plane flow of a power-law liquid induced by periodically variable pressure drop and oscillatory motion of the walls of a plane duct. Using the theory of similariry criteria of the asymptotic behaviour are formulated in four qualitatively different rheodynamic regimes. Corresponding asymptotic expressions are found for the degree of mechanical liquidization by the action of oscillatory shear stress superimposed on the principal steady state component. Theoretical results are illustrated using a set of experimental data on the gravitational flow along a vertical oscillating sheet.
AbstractPopulation protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is -hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class $${ WS}^3$$
WS
3
of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that $${ WS}^3$$
WS
3
has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership and correctness problems for $${ WS}^3$$
WS
3
reduce to solving boolean combinations of linear constraints over $${\mathbb {N}}$$
N
. This allowed us to develop the first software able to automatically prove correctness for all of the infinitely many possible inputs.
A generalized semi-Markov process with speeds describes the fluctuation, in time, of the state of a certain general system involving, at any given time, one or more living components, whose residual lifetimes are being reduced at state-dependent speeds. Conditions are given for the stationary state distribution, when it exists, to depend only on the means of some of the lifetime distributions, not their exact shapes. This generalizes results of König and Jansen, particularly to the infinite-state case.
Empirically Efficient Verification for a Class of Infinite-State Systems