Estimation of the Performance Measures of a Group of Servers Taking into Account Blocking and Call Repetition before and after Server Occupation

The model of a fully available group of servers with a Poisson flow of primary calls and the possibility of losses before and after occupying a free server is considered. Additionally, a call can leave the system because of the aging of transmitted information. After each loss, there is some probability that a customer repeats the call. Such models are seen in the modeling of various telecommunication systems such as emergency information services, call and contact centers, access nodes, etc., functioning in overloading situations. The stationary behavior of the system is described by the infinite-state Markov process. It is shown that stationary characteristics of the model can be calculated with the help of an auxiliary model of the same class but without call repetitions due to losses occurring before and after the occupation of a free server and the aging of transmitted information. The performance measurements of the auxiliary model are calculated by solving a system of state equations using a recursive algorithm based on the concept of the truncation of the used state space. This approach allows significant savings of computer resources to be made by ignoring highly unlikely states in the process of calculation. The error caused by truncation is estimated. The presented numerical examples illustrate the use of the model for the elimination of the negative effects of emergency information service overload based on the filtering of the input flow of calls.

Infinite-state graph transformation systems under adverse conditions

We present an approach for modeling adverse conditions by graph transformation systems. To this end, we introduce joint graph transformation systems which involve a system, an interfering environment, and an automaton modeling their interaction. For joint graph transformation systems, we present notions of correctness under adverse conditions. Some instances of correctness are expressible in LTL (linear temporal logic), or in CTL (computation tree logic), respectively. In these cases, verification of joint graph transformation systems is reduced to temporal model checking. To handle infinite state spaces, we incorporate the concept of well-structuredness. We discuss ideas for the verification of joint graph transformation systems using results based on well-structuredness.

Finite Element Formulation of Fractional Constitutive Laws Using the Reformulated Infinite State Representation

In this paper, we introduce a formulation of fractional constitutive equations for finite element analysis using the reformulated infinite state representation of fractional derivatives. Thereby, the fractional constitutive law is approximated by a high-dimensional set of ordinary differential and algebraic equations describing the relation of internal and external system states. The method is deduced for a three-dimensional linear viscoelastic continuum, for which the hydrostatic and deviatoric stress-strain relations are represented by a fractional Zener model. One- and two-dimensional finite elements are considered as benchmark problems with known closed form solutions in order to evaluate the performance of the scheme.

A Note on Existence of Mild Solutions for Second-Order Neutral Integro-Differential Evolution Equations with State-Dependent Delay

This article is mainly devoted to the study of the existence of solutions for second-order abstract non-autonomous integro-differential evolution equations with infinite state-dependent delay. In the first part, we are concerned with second-order abstract non-autonomous integro-differential retarded functional differential equations with infinite state-dependent delay. In the second part, we extend our results to study the second-order abstract neutral integro-differential evolution equations with state-dependent delay. Our results are established using properties of the resolvent operator corresponding to the second-order abstract non-autonomous integro-differential equation and fixed point theorems. Finally, an application is presented to illustrate the theory obtained.

Timed Trace Alignment with Metric Temporal Logic over Finite Traces

Trace Alignment is a prominent problem in Declarative Process Mining, which consists in identifying a minimal set of modifications that a log trace (produced by a system under execution) requires in order to be made compliant with a temporal specification. In its simplest form, log traces are sequences of events from a finite alphabet and specifications are written in DECLARE, a strict sublanguage of linear-time temporal logic over finite traces (LTLf ). The best approach for trace alignment has been developed in AI, using cost-optimal planning, and handles the whole LTLf . In this paper, we study the timed version of trace alignment, where events are paired with timestamps and specifications are provided in metric temporal logic over finite traces (MTLf ), essentially a superlanguage of LTLf . Due to the infiniteness of timestamps, this variant is substantially more challenging than the basic version, as the structures involved in the search are (uncountably) infinite-state, and calls for a more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution of the paper is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTLf decidability as well as on reachability for well-structured transition systems.

Temporal prophecy for proving temporal properties of infinite-state systems

Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophecy, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.