Open and Branching Behavioral Synthesis with Scenario Clauses

The Software Engineering community has identified behavioral specification as one of the main challenges to be addressed for the transference of formal verification techniques such as model checking. In particular, expressivity of the specification language is a key factor, especially when dealing with Open Systems and controllability of events and branching time behavior reasoning. In this work, we propose the Feather Weight Visual Scenarios (FVS) language as an appealing declarative and formal verification tool to specify and synthesize the expected behavior of systems. FVS can express linear and branching properties in closed and Open systems. The validity of our approach is proved by employing FVS in complex, complete, and industrial relevant case studies, showing the flexibility and expressive power of FVS, which constitute the crucial features that distinguish our approach.

Undecidability of QLTL with two variables and one monadic predicate letter

We study the algorithmic properties of the quantified linear-time temporal logic QLTL in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We prove that the satisfiability problem for QLTL in languages with two individual variables and one monadic predicate letter in Σ 11 -hard. Thus, QLTL is Π 11 -hard, and so not recursively enumerable, in such languages. The resultholds both for the increasing domain and the constant domain semantics and is obtained by reduction from a Σ 11 -hard N×N recurrent tiling problem. It follows from the proof for QLTL that similar results hold for the quantified branching-time temporal logic QCTL, and hence for the quantified alternating-time temporal logic QATL. The result presented in this paper strengthens a result by I. Hodkinson, F. Wolter, and M. Zakharyaschev, who have shown that the satisfiability problem for QLTL is Σ 11 -hard in languages with two individual variablesand an unlimited supply of monadic predicate letters.

An obstacle to sub-AdS holography for SYK-like models

We argue that “stringy” effects in a putative gravity-dual picture for SYK-like models are related to the branching time, a kinetic coefficient defined in terms of the retarded kernel. A bound on the branching time is established assuming that the leading diagrams are ladders with thin rungs. Thus, such models are unlikely candidates for sub-AdS holography. In the weak coupling limit, we derive a relation between the branching time, the Lyapunov exponent, and the quasiparticle lifetime using two different approximations.

A Game for Linear-time–Branching-time Spectroscopy

We introduce a generalization of the bisimulation game that can be employed to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. By measuring the use of expressive powers, we adapt the formula generation to just yield formulas belonging to the coarsest distinguishing behavioral preorders/equivalences from the linear-time–branching-time spectrum. The induced algorithm can determine the best fit of (in)equivalences for a pair of processes.