On Computability of Logical Approaches to Branching-Time Property Verification of Programs

2020 ◽  
Author(s):  
Takeshi Tsukada
Keyword(s):  
Branching Time ◽  
Time Property ◽  
Property Verification

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

2021 ◽  
Vol 2021 (3) ◽  
Author(s):  
Pengfei Zhang ◽  
Yingfei Gu ◽  
Alexei Kitaev
Keyword(s):  
Lyapunov Exponent ◽  
Weak Coupling ◽  
Kinetic Coefficient ◽  
Weak Coupling Limit ◽  
Branching Time ◽  
Quasiparticle Lifetime

Abstract 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.

scholarly journals Constructing weak simulations from linear implications for processes with private names

2019 ◽  
Vol 29 (8) ◽  
pp. 1275-1308 ◽  
Author(s):  
Ross Horne ◽  
Alwen Tiu
Keyword(s):  
Expressive Power ◽  
Dual Pair ◽  
Proof System ◽  
Branching Time ◽  
First Order ◽  
Order Extension

AbstractThis paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of π-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the π -calculus is established. A novel contribution of this work is that we generalise the notion of a ‘left proof’ to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal π -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.

Sign in / Sign up

Export Citation Format

Share Document