Sebastian Enqvist
We present a circular and cut-free proof system for the hybrid mu-calculus and prove its soundness and completeness. The system uses names for fixpoint unfoldings, like the circular proof system for the mu-calculus previously developed by Stirling.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We study the model-checking problem for a quantitative extension of the modal mu-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions that arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and allow the measurement of interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative mu-calculus, can be model checked with arbitrary precision on initialised l…
Deductive methods for the verification of hybrid systems vary on the format of statements in correctness proofs. Building on the example of Hoare triple-based reasoning, we have investigated several such methods for systems described in Hybrid CSP, each based on a different assertion language, notation for time, and notation for proofs, and each having its pros and cons with respect to expressive power, compositionality and practical convenience. In this paper we propose a new approach based on weakly monotonic time as the semantics for interleaving, the Duration Calculus (DC) with infinite in…
The model checking problem for open systems has been intensively studied in the literature, for both finite-state (module checking) and infinite-state (pushdown module checking) systems, with respect to Ctl and Ctl*. In this paper, we further investigate this problem with respect to the μ-calculus enriched with nominals and graded modalities (hybrid graded Mu-calculus), in both the finite-state and infinite-state settings. Using an automata-theoretic approach, we show that hybrid graded μ-calculus module checking is solvable in exponential time, while hybrid graded μ-calculus pushdown module c…
Complete Dynamic Logic of Communicating Hybrid Programs
本文为通信混合程序 dLCHP 提出相对完全的证明演算，通过结合微分动态逻辑 dL 与假设-承诺推理，并借助扩充通信轨迹的 Ω-FOD，证明了并行混合系统推理与混合、连续及离散系统推理难度完全相同。
Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics
本文提出二元混合逻辑的完备表记演算，同时构建了依赖维度的混合依赖积逻辑演算，并证明其完备性，但所有系统均不具终止性。
A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
本文提出实解析微分代数动态逻辑的证明演算，用于正确转换微分代数方程，实现微分代数方程到常微分方程的降阶，并确保与混合系统中的微分形式动态逻辑兼容。主要贡献是鬼切换，用于将多模系统分解为混合系统，正确混合复杂的微分代数动力学。
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous st…
In previous works, a tableau calculus has been defined, which constitutes a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work shows how to extend such a calculus to multi-modal logic enriched with features largely used in description logics: transitivity and relation inclusion assertions. The separate addition of either transitive relations or relation hierarchies to the considered decidable fragment of multi-modal hybrid logic can easily be shown to stay decidable, by resorting to results already proved in the literature.…
Event Calculus Meets Hybrid ASP
针对事件演算在ASP实现中面临的连续变化和值域爆炸问题，提出混合EC扩展，通过功能流和抽象步映射，利用混合ASP系统实现线性约束求解，保证终止性并支持稠密域建模。
We propose a hybrid process calculus for modelling and reasoning on cyber-physical systems (CPS{s}). The dynamics of the calculus is expressed in terms of a labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based behavioural semantics which support compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial case study.
Computational expressivity of (circular) proofs with fixed points
本文在“证明即程序”范式下研究带不动点算子的证明系统muLJ及其循环扩展CmuLJ的计算表达力，证明二者均等价于二阶算术子系统$Π^1_2$-$\mathsf{CA}_0$中的可证明全一阶函数，并给出了基于可实现性解释的下界与基于新可计算性模型的上界证明。
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous st…
HpC: A Calculus for Hybrid and Mobile Systems -- Full Version
针对物联网混合移动系统的正确性保障需求，提出经典π演算的最小保守扩展HpC，可同时刻画移动性、时间与物理特性并继承原有理论结果，通过移动设备切换协议验证了其实用性。
Complete and Terminating Tableau Calculus for Undirected Graph
本文针对无向图构造混合逻辑的表列方法，证明其完备性与终止性，并由此得出该逻辑的可判定性。
Circular Proofs as Session-Typed Processes: A Local Validity Condition
本文扩展了直觉主义线性逻辑与会话类型π演算的对应关系到带最小和最大不动点的子结构逻辑片段，提出一个局部且可判定的有效性准则来识别对应有效循环证明的互递归进程，并证明该准则比既有守护条件更严格但更适合作编程语言基础。
In a previous paper, a tableau calculus has been presented, which constitute a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work extends such a calculus to multi-modal logic with transitive relations and relation inclusion assertions. The separate addition of either transitive relations or relation hierarchies to the considered decidable fragment of multi-modal hybrid logic can easily be shown to stay decidable, by resorting to results already proved in the literature. However, such results do not directly allow for conclu…
We address a fundamental mismatch between the combinations of dynamics that occur in cyber-physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics. We provide the logical foundations for closing this analytic gap. We develop a formal model for distributed hybrid systems. It combines quantified differential equations with qu…
We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved through pattern-based blocking. Previous approaches to related logics all rely on chain-based blocking. Besides being conceptually simple and suitable for efficient implementation, the pattern-based approach gives us a NExpTime complexity bound for the decision procedure.
We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of mutually defined inductive and coinductive linear predicates. In a major case study we use it to prove the strong progress property for binary session-typed processes under an asynchronous communication semantics. As far as we are aware, this is the first proof of this property.
This paper presents a dynamic logic $d\mathcal{L}_\text{CHP}$ for compositional deductive verification of communicating hybrid programs (CHPs). CHPs go beyond the traditional mixed discrete and continuous dynamics of hybrid systems by adding CSP-style operators for communication and parallelism. A compositional proof calculus is presented that modularly verifies CHPs including their parallel compositions from proofs of their subprograms by assumption-commitment reasoning in dynamic logic. Unlike Hoare-style assumption-commitments, $d\mathcal{L}_\text{CHP}$ supports intuitive symbolic execution…
Embedding Differential Dynamic Logic in PVS
本文提出将微分动态逻辑（dL）嵌入原型验证系统（PVS）中，形式化了混合程序语义与证明演算，构建了Plaidypvs以支持在PVS内部验证混合程序并推理整类程序。
Definite Descriptions and Hybrid Tense Logic
本文构建了以谓词抽象和限定摹状词为唯一非严格词项的一阶混合时态逻辑，用处理 sat-公式的表推演演算形式化，并构造性证明插值定理，扩展了 Blackburn 与 Marx 的结果。
PDDL+ is an extension of PDDL2.1 which incorporates fully-featured autonomous processes and allows for better modelling of mixed discrete-continuous domains. Unlike PDDL2.1, PDDL+ lacks a logical semantics, relying instead on state-transitional semantics enriched with hybrid automata semantics for the continuous states. This complex semantics makes analysis and comparisons to other action formalisms difficult. In this paper, we propose a natural extension of Reiter's situation calculus theories inspired by hybrid automata. The kinship between PDDL+ and hybrid automata allows us to develop a di…
Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
本文通过结构化λ演算策略空间，证明在特定条件下eval-readback与eval-apply大步求值器的一步等价性，并系统调查策略空间。
Birkhoff style proof systems for hybrid-dynamic quantum logic
本研究基于混合与动态模态逻辑构建量子逻辑框架，提出量子子句概念及对应推理证明规则，验证了其可靠性与紧致性，并证明了该逻辑片段的Birkhoff完备性，为量子逻辑编程与形式规约提供理论支撑。
We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. In particular, we consider a practical version of the calculus called Proto-Quipper, which contains the core of Quipper. Quipper is a new quantum programming language under active development and recently has gained much popularity among the quantum computing communities. Hybrid is a system that is designed to support the use of higher-order abstract syntax (HOAS) for representing and reasoning about formal systems implemented in the Coq Proof Assistant. In th…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。