Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis

Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) assumption. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.

$$L_2$$-norm sampling discretization and recovery of functions from RKHS with finite trace

In this paper we study $$L_2$$ L 2 -norm sampling discretization and sampling recovery of complex-valued functions in RKHS on $$D \subset \mathbb {R}^d$$ D ⊂ R d based on random function samples. We only assume the finite trace of the kernel (Hilbert–Schmidt embedding into $$L_2$$ L 2 ) and provide several concrete estimates with precise constants for the corresponding worst-case errors. In general, our analysis does not need any additional assumptions and also includes the case of non-Mercer kernels and also non-separable RKHS. The fail probability is controlled and decays polynomially in n, the number of samples. Under the mild additional assumption of separability we observe improved rates of convergence related to the decay of the singular values. Our main tool is a spectral norm concentration inequality for infinite complex random matrices with independent rows complementing earlier results by Rudelson, Mendelson, Pajor, Oliveira and Rauhut.

LTLƒ Synthesis with Fairness and Stability Assumptions

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLƒ goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTLƒ goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLƒ and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTLƒ synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLƒ synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.

Efficient Model-Based Diagnosis of Sequential Circuits

In Model-Based Diagnosis (MBD), we concern ourselves with the health and safety of physical and software systems. Although we often use different knowledge representations and algorithms, some tools like satisfiability (SAT) solvers and temporal logics, are used in both domains. In this paper we introduce Finite Trace Next Logic (FTNL) models of sequential circuits and propose an enhanced algorithm for computing minimal-cardinality diagnoses. Existing state-of-the-art satisfiability algorithms for minimal diagnosis use Sorting Networks (SNs) for constraining the cardinality of the diagnostic candidates. In our approach we exploit Multi-Operand Adders (MOAs). Based on extensive tests with ISCAS-89 circuits, we found that MOAs enable Conjunctive Normal Form (CNF) encodings that are significantly more compact. These encodings lead to 19.7 to 67.6 times fewer variables and 18.4 to 62 times fewer clauses. For converting an FTNL model to CNF, we could achieve a speed-up ranging from 6.2 to 22.2. Using SNs fosters 3.4 to 5.5 times faster on-line satisfiability checking though. This makes MOAs preferable for applications where RAM and off-line time are more limited than on-line CPU time.

2-локальные изометрии некоммутативных пространств Лоренца

Let mathcal M be a von Neumann algebra equipped with a faithful normal finite trace tau, and let Sleft( mathcalM, tauright) be an ast -algebra of all tau -measurable operators affiliated with mathcal M . For x in Sleft( mathcalM, tauright) the generalized singular value function mu(x):trightarrow mu(tx), t0, is defined by the equality mu(tx)infxp_mathcalM:, p2pp in mathcalM, , tau(mathbf1-p)leq t. Let psi be an increasing concave continuous function on 0, infty) with psi(0) 0, psi(infty)infty, and let Lambda_psi(mathcal M,tau) left x in Sleft( mathcalM, tauright): x _psi int_0inftymu(tx)dpsi(t) infty right be the non-commutative Lorentz space. A surjective (not necessarily linear) mapping V:, Lambda_psi(mathcal M,tau) to Lambda_psi(mathcal M,tau) is called a surjective 2-local isometry, if for any x, y in Lambda_psi(mathcal M,tau) there exists a surjective linear isometry V_x, y:, Lambda_psi(mathcal M,tau) to Lambda_psi(mathcal M,tau) such that V(x) V_x, y(x) and V(y) V_x, y(y). It is proved that in the case when mathcalM is a factor, every surjective 2-local isometry V:Lambda_psi(mathcal M,tau) to Lambda_psi(mathcal M,tau) is a linear isometry.

Oscillation Theory for the Density of States of High Dimensional Random Operators

Sturm–Liouville oscillation theory is studied for Jacobi operators with block entries given by covariant operators on an infinite dimensional Hilbert space. It is shown that the integrated density of states of the Jacobi operator is approximated by the winding of the Prüfer phase w.r.t. the trace per unit volume. This rotation number can be interpreted as a spectral flow in a von Neumann algebra with finite trace.

Worst Case Branching and Other Measures of Nondeterminism

Many nondeterminism measures for finite automata have been studied in the literature. The tree width of an NFA (nondeterministic finite automaton) counts the number of leaves of computation trees as a function of input length. The trace of an NFA is defined in terms of the largest product of the degrees of nondeterministic choices in computations on inputs of given length. Branching is the corresponding best case measure based on the product of nondeterministic choices in the computation that minimizes this value. We establish upper and lower bounds for the trace of an NFA in terms of its tree width. We give a tight bound for the size blow-up of determinizing an NFA with finite trace. Also we show that the trace of any NFA either is bounded by a constant or grows exponentially.