Transpension: The Right Adjoint to the Pi-type

Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to make the resulting language more expressive, or in order to carry out further reasoning internally, allowing greater abstraction and sometimes automated verification. While the constructions of presheaf models largely follow a common pattern, approaches towards internalization do not. Throughout the literature, various internal presheaf operators ($\surd$, $\Phi/\mathsf{extent}$, $\Psi/\mathsf{Gel}$, $\mathsf{Glue}$, $\mathsf{Weld}$, $\mathsf{mill}$, the strictness axiom and locally fresh names) can be found and little is known about their relative expressivenes. Moreover, some of these require that variables whose type is a shape (representable presheaf, e.g. an interval) be used affinely. We propose a novel type former, the transpension type, which is right adjoint to universal quantification over a shape. Its structure resembles a dependent version of the suspension type in HoTT. We give general typing rules and a presheaf semantics in terms of base category functors dubbed multipliers. Structural rules for shape variables and certain aspects of the transpension type depend on characteristics of the multiplier. We demonstrate how the transpension type and the strictness axiom can be combined to implement all and improve some of […]

Published on June 19, 2024
An implicit function theorem for the stream calculus

In the context of the stream calculus, we present an Implicit Function Theorem (IFT) for polynomial systems, and discuss its relations with the classical IFT from calculus. In particular, we demonstrate the advantages of the stream IFT from a computational point of view, and provide a few example applications where its use turns out to be valuable.

Published on June 18, 2024
On the Metric Temporal Logic for Continuous Stochastic Processes

In this paper, we prove measurability of event for which a general continuous-time stochastic process satisfies continuous-time Metric Temporal Logic (MTL) formula. Continuous-time MTL can define temporal constrains for physical system in natural way. Then there are several researches that deal with probability of continuous MTL semantics for stochastic processes. However, proving measurability for such events is by no means an obvious task, even though it is essential. The difficulty comes from the semantics of "until operator", which is defined by logical sum of uncountably many propositions. Given the difficulty involved in proving the measurability of such an event using classical measure-theoretic methods, we employ a theorem from stochastic analysis. This theorem is utilized to prove the measurability of hitting times for stochastic processes, and it stands as a profound result within the theory of capacity. Next, we provide an example that illustrates the failure of probability approximation when discretizing the continuous semantics of MTL formulas with respect to time. Additionally, we prove that the probability of the discretized semantics converges to that of the continuous semantics when we impose restrictions on diamond operators to prevent nesting.

Published on June 13, 2024
Linear-time logics -- a coalgebraic perspective
Authors: Corina Cirstea.

We describe a general approach to deriving linear-time logics for a wide variety of state-based, quantitative systems, by modelling the latter as coalgebras whose type incorporates both branching and linear behaviour. Concretely, we define logics whose syntax is determined by the type of linear behaviour, and whose domain of truth values is determined by the type of branching behaviour, and we provide two semantics for them: a step-wise semantics akin to that of standard coalgebraic logics, and a path-based semantics akin to that of standard linear-time logics. The former semantics is useful for model checking, whereas the latter is the more natural semantics, as it measures the extent with which qualitative properties hold along computation paths from a given state. Our main result is the equivalence of the two semantics. We also provide a semantic characterisation of a notion of logical distance induced by these logics. Instances of our logics support reasoning about the possibility, likelihood or minimal cost of exhibiting a given linear-time property.

Published on June 13, 2024
Branch-Well-Structured Transition Systems and Extensions

We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from another. Furthermore, the monotony condition is relaxed in the same way. While this retains the decidability of non-termination and boundedness, it appears that the coverability problem is undecidable. To this end, we define a new notion of monotony, called cover-monotony, which is strictly more general than the usual monotony and still allows us to decide a restricted form of the coverability problem.

Published on June 12, 2024

Managing Editors


Stefan Milius

Brigitte Pientka
Fabio Zanasi
Executive Editors

Editorial Board
Executive Board

eISSN: 1860-5974

Logical Methods in Computer Science is an open-access journal, covered by SCOPUS, DBLPWeb of Science, Mathematical Reviews and Zentralblatt. The journal is a member of the Free Journal Network. All journal content is licensed under a Creative Commons license.