TCTL Inevitability Analysis of Dense-time Systems

Farn Wang; Geng-Dian Hwang; Fang Yu

Home/Archive/arXiv

arXiv · cs/0304003

TCTL Inevitability Analysis of Dense-time Systems

Farn Wang·Geng-Dian Hwang·Fang Yu

View original source ↗Read source document ↗Export metadata ↓

Abstract

Inevitability properties in branching temporal logics are of the syntax forall eventually ϕ, where ϕis an arbitrary (timed) CTL formula. In the sense that "good things will happen", they are parallel to the "liveness" properties in linear temporal logics. Such inevitability properties in dense-time logics can be analyzed with greatest fixpoint calculation. We present algorithms to model-check inevitability properties both with and without requirement of non-Zeno computations. We discuss a technique for early decision on greatest fixpoints in the temporal logics, and experiment with the effect of non-Zeno computations on the evaluation of greatest fixpoints. We also discuss the TCTL subclass with only universal path quantifiers which allows for the safe abstraction analysis of inevitability properties. Finally, we report our implementation and experiments to show the plausibility of our ideas.

Explore related subjects

cs.SC

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Farn Wang, Geng-Dian Hwang, Fang Yu. 2003-05-20. TCTL Inevitability Analysis of Dense-time Systems. https://arxiv.org/abs/cs/0304003

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Construction and formal verification of a special topology on {\mathbb{Z}}^{n}: characterization of connected subsets

We examine whether the integers admit a topology whose connected subsets are precisely the sets of consecutive integers. The main result gives a construction for every integer lattice {\mathbb{Z}}^{n}, n>0; the answer for Z is then obtained as a corollary. We prove that the neighborhoods determined by the parity of the sum of the coordinates form a basis and that topological connectedness agrees exactly with accessibility by finite paths of unit lattice steps. We also present a deductive audit and the correspondence between this argument and a verification in Lean 4 and Mathlib, including the empty set and the independent formal characterization of integer intervals. The construction and mathematical result originate in Problem 5712, proposed by Dan Marcus and solved in 1970 by the Cleveland State University group; the present article contributes a detailed exposition and a report on formal verification.

cs.SC↗

arXiv2026

On the Complexity of Computing with p-adic Lattices

We study the complexity of two fundamental problems attached to p-adic lattices: computing an N-orthogonal basis, and deciding whether a given basis is N-orthogonal. When the norm is supplied through an explicit diagonal representation, both problems are polynomial. However, in the black-box model, where the ultrametric norm N is fixed and only accessible through an evaluation oracle, we prove that both problems require $Ω$(p^{v-1} ) queries in the worst case, where v $\le$ n is the largest multiplicity of a commensurability class of N and n is the dimension of the ambient vector space. We then analyse the optimality of these bounds by providing explicit algorithms. Our results answer formally an open question of Zhang, Deng and Wang and refine the recent results of Duan and Wu by providing pointwise query bounds depending on the norm's structure, in addition to uniform bounds.

cs.SC↗

arXiv2026

Barik transform and Barik eliminant: a novel algebraic method to solve polynomial equations in the sine and cosine of one variable

Systems of trigonometric equations appear frequently in problems related to geometry, kinematics, computer graphics, robotics, and astronomy, among many other fields. Most often these are first converted to algebraic equations via the ``tangent half-angle'' substitution and solved subsequently using various algebraic methods, such as computation of resultants. In the process, parametric singularities are introduced in the equations, and their degrees are also doubled. In this article, a novel concept call the ``Barik transform'' is introduced, which can help solve such a system without encumbering these issues, albeit only in systems that contain {\em at least} one equation of the first degree in the sine and cosine of the variable to be eliminated. It is shown how Barik transform can produce extremely compact eliminants in the closed form, without resorting to any resultant computation.

cs.SC↗