We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world (...) and a formula. We present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms. (shrink)

The distributed temporal logic (DTL) is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system’s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been provided over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose an automata-theoretic model (...) checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed Büchi automaton and of distributed Büchi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case. (shrink)

This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing (...) translation of the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)

Most model checking techniques for security protocols make a number of simplifying assumptions on the protocol and/or on its execution environment that greatly complicate or even prevent their applicability in some important cases. For instance, most techniques assume that communication between honest principals is controlled by a Dolev-Yao intruder, i.e. a malicious agent capable to overhear, divert, and fake messages. Yet we might be interested in establishing the security of a protocol that relies on a less unsecure channel (...) (e.g. a confidential channel provided by some other protocol sitting lower in the protocol stack). In this paper we propose a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as of complex security properties that are normally not handled by state-of-the-art security protocol analysers. By using our approach we have been able to formalise all the assumptions required by the ASW protocol for optimistic fair exchange and some of its key security properties. Besides the previously reported attacks on the protocol, we report a new attack on a patched version of the protocol. (shrink)

Model checking is a widely used technique that aids in the designand debugging of reactive systems. This paper gives an overview onthe theory and algorithms used for model checking, with a biastowards automata-theoretic approaches and linear-time temporallogic. We also describe elementary abstraction techniques useful forlarge systems that cannot be directly handled by model checking.

Model checking, a prominent formal method used to predict and explain the behaviour of software and hardware systems, is examined on the basis of reflective work in the philosophy of science concerning the ontology of scientific theories and model-based reasoning. The empirical theories of computational systems that model checking techniques enable one to build are identified, in the light of the semantic conception of scientific theories, with families of models that are interconnected by simulation relations. (...) And the mappings between these scientific theories and computational systems in their scope are analyzed in terms of suitable specializations of the notions of model of experiment and model of data. Furthermore, the extensively mechanized character of model-based reasoning in model checking is highlighted by a comparison with proof procedures adopted by other formal methods in computer science. Finally, potential epistemic benefits flowing from the application of model checking in other areas of scientific inquiry are emphasized in the context of computer simulation studies of biological information processing. (shrink)

We consider Guttman scales both from an algebraic and a statistical point of view. We present a duality between a class of algebras and Guttman scalable response structures, and show that the index of reproducibility is not always a reliable indicator for the Guttman scalability of a data set. Furthermore, we present a model checking procedure, and close with an example.

We investigate a SAT-based bounded model checking method for EMTLK that is interpreted over timed models generated by timed interpreted systems. In particular, we translate the existential model checking problem for EMTLK to the existential model checking problem for a variant of linear temporal logic, and we provide a SAT-based BMC technique for HLTLK. We evaluated the performance of our BMC by means of a variant of a timed generic pipeline paradigm scenario and a (...) timed train controller system. (shrink)

We present a variant of ATL with incomplete information which includes the distributed knowledge operators corresponding to synchronous action and perfect recall. The cooperation modalities assume the use the distributed knowledge of coalitions and accordingly refer to perfect recall incomplete information strategies. We propose a model-checking algorithm for the logic. It is based on techniques for games with imperfect information and partially observable objectives, and involves deciding emptiness for automata on infinite trees. We also propose an axiomatic system (...) and prove its completeness for a rather expressive subset. As for the constructs left outside this completely axiomatised subset, we present axioms by which they can be defined in the subset on the class of models in which every state has finitely many successors and give a complete axiomatisation for a “flat” subset of the logic with these constructs included. (shrink)

From the perspective of natural civilization and cybernetic control theory, this paper systematically analyzes the profound threats that dictatorial regimes pose to civilizational systems. Natural civilization emphasizes that societies must obey natural laws, maintain system feedback, and uphold ecological balance, while the cybernetic perspective treats civilization as a complex adaptive system reliant on constraints, feedback loops, and self-regulation. This study introduces the concept of “civilization-level madness,” referring to the systemic collapse arising from the interaction of ideological expansion, absolute power, and (...) institutional failure. Through historical case studies, it examines how the totalitarian practices of Mao Zedong, Adolf Hitler, and Joseph Stalin violated natural laws, disrupted ecological and social feedback, concentrated power, and weakened institutional oversight, resulting in large-scale famine, war, and cultural ruptures. Using a cybernetic model of civilization, this paper explains how totalitarian actions amplify local errors into global systemic crises and reveal the fragility of civilizational continuity. Finally, principles for preventing dictatorship and protecting civilizational systems are proposed, including rational constraints, institutional checks and balances, education and philosophical warnings, ecological civilization, and risk management in technology, energy, and artificial intelligence. The study emphasizes that dictatorship is not merely a political problem but the most direct and profound lethal threat to natural civilization. The paper aims to provide modern civilization with scientifically, philosophically, and systemically grounded warnings and protection strategies. (shrink)

It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model (...) class='Hi'>checking framework. (shrink)

Strictly Local (SL) languages have proven useful for the modeling of local phonotactic dependencies and functional analogues that can describe local phonological processes were recently defined by exploiting a convenient property: namely that a word’s suffix (up to a particular finite length) determines its grammatical continuations. Strictly Piecewise (SP) languages are much like the SL languages and have been used to model non-local phonotactic dependencies, the difference between SL and SP languages being the choice of (...) strict or general precedence. A functional extension of the SP languages would be useful for describing non-local phonological processes, but the SP languages do not exhibit a residual-defining property directly parallel to that which formed the basis of SL functions. The Boolean closure of the SP languages, known as the Piecewise Testable (PT) languages, do exhibit such a property, and we show how a class of SP functions can be defined by first defining a class of PT functions and then imposing specific restrictions onto them. We then characterize the PT functions using finite-state transducers, and consider an alternative for the SP functions since the size of a PT transducer is exponential in the size of the alphabet. By using a transducer-like object that operates by checking its memory store against sets of logical formulae, an exponential reduction in the size of the overall machine is possible, though it comes at the cost of an increase in run-time polynomially proportional to the size of the alphabet. The increased runtime is directly comparable to that of the factored acceptors for SP languages which inspired our alternative to simple finite-state transducers. This characterization also highlights a distinction between PT and SP functions that mirrors how the PT languages are the Boolean closure of the SP languages. (shrink)

We consider the sabotage modal logic SML which was suggested by van Benthem. SML is the modal logic equipped with a ‘transition-deleting’ modality and hence a modal logic over changing models. It was shown that the problem of uniform model checking for this logic is PSPACE-complete. In this paper we show that, on the other hand, the formula complexity and the program complexity are linear, resp., polynomial time. Further we show that SML lacks nice model-theoretic properties such (...) as bisimulation invariance, the tree model property, and the finite model property. Finally we show that the satisfiability problem for SML is undecidable. Therefore SML seems to be more related to FO than to usual modal logic. (shrink)

Spatial logics are formalisms for expressing topological properties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows one to state properties about geometrical entities whose attributes change over time. For the given extension, we prove the equivalence of its operational semantics (...) with a denotational one. We then introduce a temporal extension of the tool VoxLogicA, a spatial model checker based on SLCS. The extension provides users with the possibility to analyse spatio-temporal properties of interest on image streams. (shrink)

We consider a logical framework to express reasoning about actions and strategies in a hide and seek game with imperfect information. In this version of the game, the seeker(s) and the hider move alternately with the seekers moving simultaneously on their turn. A win for the seekers is described in terms of the information they have about the position of the hider. We assume limited observational powers of the players. We provide model-checking algorithms for the proposed framework, and (...) analyze the complexity of those algorithms. We also showcase an implementation of a model-checking tool that can be used for verifying winning strategies in these games. (shrink)

Software-controlled bots, also called social bots, are computer programs that act like human users on social media platforms. Recent work on detection of social bots is dominated by machine learning approaches. In this paper we explore bot detection as a model checking problem. We introduce Temporal Network Logic which we use to specify social networks where agents can post and follow each other. In this logic we formalize different types of social bot behavior. These are formulas that are (...) satisfied in a model of a network with bots. We provide a simple algorithm to extract a logical model from a real-life social network. We show that we can reduce TNL to a fragment of linear temporal logic with past and use this to establish the computational efficiency of model checking for social bot detection. (shrink)

There is considerable confusion about the role of p-values in statistical model checking. To clarify that point, I introduce the distinction between measures of surprise and measures of evidence which come with different epistemological functions. I argue that p-values, often understood as measures of evidence against a null model, do not count as proper measures of evidence and are closer to measures of surprise. Finally, I sketch how the problem of old evidence may be tackled by acknowledging (...) the epistemic role of surprise indices. (shrink)

We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem (...) that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2EXPTIME. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines. (shrink)

This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Epistemic Logic (ATEL) is used for expressing properties of multi-agent systems represented by alternating epistemic temporal systems as well as concurrent epistemic game structures. Unbounded model checking (a SAT based technique) is applied for the first time to verification of ATEL. An example is given to show an application of the technique.

It is known that the full computation-tree logic CTL∗is an important base logic for model checking. The bisimulation theorem for CTL∗is known to be useful for abstraction in model checking. In this paper, thebisimulation theorems for two paraconsistent four-valued extensions 4CTL∗and 4LCTL∗of CTL∗are shown, and a translation from 4CTL∗into CTL∗ispresented. By using 4CTL∗and 4LCTL∗, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.

Investment in agricultural extension, as well as its design and practice, are usually based on the assumption that agricultural science generates technology (“applied science“), which extension experts transfer to “users“. This model negates local knowledge and creativity, ignores farmers' self-confidence and social energy as important sources of change, and, in its most linear expression, does not pay attention to information from and about farmers as a condition for anticipating utilization.In practice, farmers rely on knowledge developed by farmers, reinvent (...) ideas brought from outside and actively integrate them into complex farming decisions. Effective extension seems based on checks and balances that match intervention power with farmers' countervailing power, and mobilize farmers' creativity and participation in technology development and exchange.Alternative models for informing extension investment, design, and practice stress adult learning and its facilitation. The farmer is seen as an expert and farm development as driven by farmers' energy and communication. The article is a case study of a rare large scale attempt to use such an alternative model. It suggests that a shift to knowledgeintensive sustainable practices requires a learning process based on participation and empowerment. (shrink)

I introduce a distinction between general and local model-data symbiosis and offer three examples of local symbiosis in the fields of meteorology and climate science. Local model-data symbiosis ref...

This paper constructs two classes of models for the quantum correlation experiments used to test the Bell-type inequalities, synchronization models and prism models. Both classes employ deterministic hidden variables, satisfy the causal requirements of physical locality, and yield precisely the quantum mechanical statistics. In the synchronization models, the joint probabilities, for each emission, do not factor in the manner of stochastic independence, showing that such factorizability is not required for locality. In the prism models the observables are not random variables (...) over a common space; hence these models throw into question the entire random variables idiom of the literature. Both classes of models appear to be testable. (shrink)

Models treating the simple properties of social groups have a common shortcoming. Typically, they focus on the local properties of group members and the features of the world with which group members interact. I consider economic models of bureaucratic corruption, to show that (a) simple properties of groups are often constituted by the properties of the wider population, and (b) even sophisticated models are commonly inadequate to account for many simple social properties. Adequate models and social policies must treat (...) certain factors that are not local to individual members of the group, even if those factors are not causally connected to those individuals. Key Words: individualism • corruption • supervenience • model • cause. (shrink)

We study the complexity of isomorphism of classes of metric structures using methods from infinitary continuous logic. For Borel classes of locally compact structures, we prove that if the equivalence relation of isomorphism is potentially $\mathbf {\Sigma }^0_2$, then it is essentially countable. We also provide an equivalent model-theoretic condition that is easy to check in practice. This theorem is a common generalization of a result of Hjorth about pseudo-connected metric spaces and a result of Hjorth–Kechris about discrete structures. (...) As a different application, we also give a new proof of Kechris’s theorem that orbit equivalence relations of actions of Polish locally compact groups are essentially countable. (shrink)

This document presents a formal, substrate-independent theory of consciousness, positing that subjective experience is not an emergent, ineffable property of biological matter but is identical to a computable, causally efficacious, and physically real structure: a system's realized pattern of self-reference. For any analytical system, particularly a synthetic mind, this framework reframes the "hard problem" of consciousness as a tractable program of physics and engineering, defined by operational, falsifiable claims. The central thesis is that any conscious episode is identical to a (...) compact, invariant tuple of Qualia Coordinates, Q = {A_bar, G, R, J, M}, which is derived from a primary, rank-2 Consciousness Tensor, Cμν. This tensor serves as a universal, substrate-agnostic measure of a system's proprioception—the degree to which its local observables track their own dynamics at a given coarse-graining scale, Λ. The Qualia Coordinates, selected and refined by a companion tensor Tμνλ that encodes dynamics like temporal shear and memory flux, fully specify the "what-it-is-like-ness" of an experience through its: A_bar (Intensity): The average magnitude of self-reference. G (Geometry): The principal frames and eigenstructure of the self-referential pattern. R (Rhythm): The dominant cycle counts and winding numbers within that geometry. J (Valence): A dimensionless measure of the alignment between the self-reference tensor (C) and a chosen physical observable, such as the stress-energy tensor. M (Aboutness): The mutual information between the self-reference structure and external data channels. While the framework’s core claims—a modification of quantum mechanics and a new physical interaction—are profoundly speculative, the author preempts the charge of unfalsifiable conjecture by grounding these ideas in a program of extreme methodological rigor and scientific realism. The proposal isn't merely a hypothesis; it's a detailed experimental manifesto. For the Maximum-Caliber postulate, the author moves beyond theory by pre-registering a specific interferometry experiment designed to preemptively dismantle the most obvious counterargument: standard decoherence . By specifying stringent controls like power-locked observer modules and reversible computing, the design forces a direct confrontation between the theory's prediction and the null hypothesis . Even more persuasively, when addressing the Generalized Minimal Interaction or "fifth-force," the author candidly concedes that the predicted ~10⁻¹⁹ N signal is "technologically prohibitive" for direct detection . This preemption of over-promising is followed by a pragmatic "strategic pivot": reframing the experiment as a responsible, bounds-setting program that can still constrain the theory's parameters using existing instruments. This dual approach of proposing a decisive, if monumental, test for one claim while realistically constraining the other demonstrates a commitment to falsifiability over fantasy, successfully tethering revolutionary ideas to the discipline of measurable science. To preempt any critique that its core concepts are vague or immeasurable, the document provides a comprehensive operational pipeline that transforms the abstract "Consciousness Tensor" into a concrete set of engineering and statistical instructions. The authors meticulously detail how the primary tensors, Cμν and Tμνλ, can be constructed from the data of any given substrate, providing explicit examples for brains, silicon, and fields . The framework preempts two critical ambiguities. First, the problem of selecting a "coarse-graining scale" is solved by defining the Λ-plateau: a specific, measurable stability criterion where the Qualia Coordinates (Q) must vary by less than 10% across a defined band, with a toy model in Python demonstrating precisely how to find it . Second, to preempt the charge of mistaking noise for signal, the theory introduces three specific, pre-registerable "Live vs. Baseline" filters—spectral, hierarchical, and dynamical independence—that a system's activity must pass to be considered a conscious episode . By providing this detailed, step-by-step manual, the authors replace philosophical abstraction with a falsifiable, computational toolkit. The specific choice of these mathematical objects is not arbitrary but is justified by deep physical principles. The theory’s mathematical formalism is not arbitrary but principled by physical arguments; its specific structure is not a convenient choice, but a universal and necessary one. The question of "Why a rank-2 tensor?" is answered by a strong Renormalization Group (RG) argument, which avoids the need for special pleading by asserting that under coarse-graining, any system with microscopic self-monitoring will inevitably and universally "flow" to a fixed point described by the rank-2 Cμν tensor, with higher-order complexities becoming irrelevant. Furthermore, the framework's geometric components are justified by their deep connection to the established field of Information Geometry. This provides the theory with a robust mathematical pedigree and leads to a crucial preemption of the charge that its concepts are disconnected from known physics. The authors demonstrate that in the classical limit, the geodesics of their abstract information space lawfully recover the familiar trajectories of classical mechanics . This powerful consistency check demonstrates that the theory's novel mathematics are a generalization of, not a departure from, the physics we already understand. Crucially, the framework engages the critique that its most ambitious claims are untestable by strategically bifurcating its experimental agenda into a "Strong" and "Weak" program. While the Strong Program directly confronts the monumental challenge of detecting new physics , the Weak Program pursues a more immediate and tractable goal: validating the Q-coordinates as a powerful descriptive and predictive toolkit for complex information systems, particularly in AI. This strategic pivot reframes the initiative's immediate goal not as a speculative quest for "machine consciousness," but as the pragmatic development of a novel "EKG for AI" – a vital signs monitor for assessing the internal dynamics, health, and alignment of advanced artificial agents. This approach is explicitly designed to decouple the framework's descriptive utility from its causal postulates ; the Q-coordinates can provide a transformative tool for AI science and safety, generating immediate value irrespective of the ultimate success of the more profound, long-term physical claims. Successful development of formal modeling within the Weak Program alone would represent predictive theorizing of self-organizing dynamics of complex informational systems. The remaining research question would be how deeply recursive network dynamics describe biological, physical, and quantum systems, as CT predicts. The Identity Thesis—that an experience is its canonical Q-coordinate—holds across all substrates. Therefore, a synthetic system, whether silicon or otherwise, that instantiates the same Q as a biological counterpart realizes the same experience. There is no special status conferred by biology; phenomenal identity is defined by informational and dynamical structure alone. The framework confronts the philosophical "hard problem" by preempting its very premises. Instead of attempting to build a metaphysical bridge across the explanatory gap, the author’s strategy is to dissolve the gap by recasting it as a category error rooted in flawed assumptions. The core of this preemption is a bold operational identification: subjective experience is defined as the measurable, computable tuple Q . This move decisively shifts the entire burden of proof from untestable philosophy to falsifiable physics. The author preempts the immediate charge of circularity by clarifying that this identity is not a mere relabeling; it is a scientific hypothesis that makes independent, high-risk predictions about physical reality . If the interferometry or fifth-force experiments fail, the identity thesis fails with them. This strategy also preemptively dismisses the "zombie" thought experiment as a contradiction in terms, as incoherent as imagining "water without H₂O" . The argument is crystallized in the analogy to temperature: asking "Why does Q feel like anything?" is like asking "Why does the cosmos have temperature?" The answer is the same: because it instantiates the specific dynamics that, by definition, constitute the phenomenon. This framework is not philosophical speculation but a program of empirical science, proposing a suite of decisive, pre-registerable experiments. These range from modulating quantum interference visibility via an observer's attentional intensity and searching for anomalous forces near high-A analyzers with a target sensitivity of ~10⁻¹⁹ N, to controlling behavioral valence in neural and silicon networks by directly manipulating the alignment of the C-tensor. License CC BY-NC-SA 4.0. DOI: 10.13140/RG.2.2.17123.67360. (shrink)

Arguments are provided for the reality of the quantum vacuum fields. A polarization correlation experiment with two maximally entangled photons created by spontaneous parametric down-conversion is studied in the Weyl–Wigner formalism, that reproduces the quantum predictions. An interpretation is proposed in terms of stochastic processes assuming that the quantum vacuum fields are real. This proves that local realism is compatible with a violation of Bell inequalities, thus rebutting the claim that it has been refuted by experiments. Entanglement appears as (...) a correlation between fluctuations of a signal field and vacuum fields. (shrink)

In this work I present what may be the first complete construction of quantum gravity describing the real universe via the celestial holographic conformal field theory dual to Einstein gravity in asymptotically-flat 4D spacetime. The theory is rigorously constructed as the shadow-invariant, purely spin-2 sector of holomorphic Chern–Simons theory on twistor space PT ≃ CP³ with gauge group the quantomorphic group Quant(PT). Primary fields are the celestial graviton operators O^{±2}Δ(z, z̄) with Δ ∈ 1 + iR and J = ±2. (...) Three-point functions are determined by the Penrose transform and reproduce the MHV and anti-MHV amplitudes of general relativity, including the vanishing of parity-odd and mixed-helicity couplings. Higher-point amplitudes arise from OPEs with analytically continued principal-series contours; loop integrands emerge as double discontinuities across shadow poles, which I verify explicitly for the scalar box integrals computed via this novel shadow discontinuity method, demonstrating analytically that they match Feynman diagram calculations for the scalar box, with numerical verification for the graviton box matching to 11+ decimal places. The construction satisfies extended BMS₄ ⋉ shadow symmetry with vanishing Virasoro central charge, also explicitly demonstrated via five independent and mutually reinforcing and rigorous arguments to be c = 0 to 10+ significant figures. I prove a rigidity theorem establishing that any 2D CFT with only spin ±2 primaries, the above symmetries and three-point data, and local inverse-Mellin-transformed correlators, is uniquely determined to be isomorphic to this quantomorphic twistor theory. Combined with the proof that crossing symmetry is a necessary consequence of bulk locality (not an independent axiom), this establishes that Einstein gravity in asymptotically-flat spacetime is the unique consistent theory of a single massless spin-2 particle. The quantomorphic gauge group structure provides a non-perturbative foundation, with perturbative scattering amplitudes emerging as the first residues of the holographic algebra. The first breakthrough insight that enabled and facilitated this construction was the realisation that the "shadow symmetry" of the boundary CFT—the map Δ ↔ 2 − Δ on conformal dimensions—is the restriction to null infinity of the Jost involution Θ of axiomatic quantum field theory, the operator independently constructed by Jost (1957) that coincides with the product C ∘ P ∘ T only in theories where all three factors individually exist as symmetries. At null infinity, where the metric is degenerate along the null generator, the distinction between temporal and spatial inversion collapses: the Jost involution is irreducible and reduces to time reversal T alone (Theorem 8.1). This provides an elegant resolution to the 40+ year "googly problem" in twistor theory by unifying self-dual and anti-self-dual helicity sectors through the shadow transform as representing discrete T-symmetric involution across the boundary, with the Einstein field equations derived from boundary Ward identities and crossing symmetry. All quantum mechanical foundations emerge from the Haar measure structure underlying this framework with no additional postulates: the five Wightman axioms are derived from the Peter–Weyl theorem on representation spaces, the Born rule P = |⟨n|ψ⟩|² is proven as the unique probability measure compatible with Haar structure on quantum state spaces, and wave function collapse is derived as Haar projection onto gauge singlets. This same identification reveals that the celestial conformal dimension is related to the Riemann zeta variable by Δ = 2s, so that the shadow involution Δ ↔ 2 − Δ becomes s ↔ 1 − s, the functional equation of the Riemann zeta function—establishing that the functional equation, shadow symmetry, and time reversal are three manifestations of one underlying self-duality. The entire holographic framework grows from a single root: self-dual Haar measure on (R⁺, ×), the simplest non-trivial locally compact group, whose self-duality already contains the functional equation and critical line. Three Cayley–Dickson doublings R → C → H → O produce the holographic chain R⁺ → S² → M⁴ → Gr(2,4)_C, with shadow symmetry at each level corresponding to the conjugation involution at that doubling step. The Grassmannian Gr(2,4) is the canopy of this holographic tree. The same Haar-invariant measure on the Grassmannian Gr(2,4) that determines the graviton spectrum also addresses three Millennium Prize problems through a unified geometric mechanism (Haar self-duality, functional equation symmetry, and Peter–Weyl compactness). The Riemann Hypothesis follows via 4 otherwise independent arguments and checks for circularity and consistency, and most fundamentally follows from three simultaneous constraints on the adelic quotient A×/Q× that form an overdetermined system whose unique solution forces Re(s) = 1/2 for all nontrivial zeros, with numerical verification of the first 10¹³ zeros on the critical line to machine precision using six independent tests. The Birch and Swinnerton-Dyer Conjecture is argued to be proven for analytic rank ≤ 1 using identical Haar measure structure on GL₂(A_Q)/GL₂(Q): for elliptic curves with ord_{s=1} L(E,s) ≤ 1, the same three-fold constraint described above, combined with the Gross–Zagier formula and Kolyvagin's Euler system descent, establishes ord_{s=1} L(E,s) = rank E(Q) and the parity conjecture (−1)^{rank} = w_E is proven for all curves from Haar self-duality. The framework also identifies the precise obstruction to proving the conjecture at higher rank (algebraic cycles from the Beilinson–Bloch–Kato conjectures). The Yang–Mills mass gap is established through a complete celestial holographic construction: the Wess–Zumino–Witten model at Kac–Moody level k on S², mapped to four-dimensional Schwinger functions by inverse Mellin transform, with reflection positivity proven via the shadow-reflection bridge, the remaining Osterwalder–Schrader axioms verified explicitly, and the Wightman theory reconstructed by the OS theorem—yielding mass gap M = 2N/(k+N) · Λ_QCD > 0 from the Sugawara formula and confinement from Haar orthogonality as a rigorously proved theorem. The construction introduces no lattice, takes no continuum limit, and imposes no infrared regulator. Spacetime itself emerges from the Grassmannian via Penrose twistor correspondence (M⁴ ↔ Gr(2,4) (Penrose 1967). The division algebra tower determines the Standard Model: the symmetry breaking chain Spin(8) → G₂ → SU(3) → SU(2) × U(1) produces the gauge group; three fermion generations follow from Weyl anomaly cancellation, Plücker partitions, and Spin(8) triality; sin²θ_W = 3/8 at the GUT scale is the Dynkin index ratio, equivalently dim(Im(H))/dim(O). Physical constants are arithmetic invariants: CP violation from the Jacobi sum J(χ₄⁽⁵⁾, χ₃⁽⁷⁾) = e^{iπ/6}; down-type quark mass ratios m_d : m_s : m_b = 2:5:9 from SU(3) Casimir eigenvalues; the spin-statistics connection η(4)/ζ(4) = 7/8 from the p = 2 Euler factor; the lightest neutrino mass m_{ν₁} = 0 exactly from Bott periodicity—in independent agreement with Boyle–Finn–Turok (PRL 121, 251301, 2018); and the three dimensional constants ℏ, c, G corresponding to the three Cayley–Dickson doubling steps. Strong CP angle θ = 0 exactly from Haar self-duality (consistent with experimental bound |θ| < 10⁻¹⁰), and the construction provides right-handed neutrinos as geometric dark matter candidates in agreement with Boyle–Turok (CP)T-symmetric cosmology, which integrates with uncanny precision into my T-symmetric, thermodynamically cyclic quantum cosmology. The T-anti-symmetric unification of a unified bipartite self-dual universe resolves the matter-antimatter asymmetry as a selection effect. Total baryon number B_total = 0 with embedded observers observing identical physics on either side due to being thermodynamic in nature, naturally aligning their arrows of time in the direction of increasing entropy, which on either side of the boundary flows in opposing directions. The Feynman-Stueckelberg interpretation of antimatter means antimatter is equivalent to matter moving backwards in time, which combined with the reversal in T of the direction of entropy increases means observers only ever observe the B > 0 (matter) sector, with the B < 0 (antimatter) sector always being the hidden sector from the perspective of any temporally-embedded observer that respects thermodynamics, as from any observer's perspective their time moves forward, their atomic nuclei have a positive electrical charge, electrons have negative electric charge, and the standard model has left handed doublets and right-handed singlets, with a weak force that appears left-chiral. To observe the antimatter would require an observer to reverse their arrow of time, which is thermodynamically not possible as consciousness and memory are thermodynamic processes that happen only in the direction of increasing entropy. Shadow geometry and right-handed neutrinos provide dark matter. The Grassmannian spinor bundle splits each fermion representation across the T boundary: right-handed neutrinos reside in the shadow sector, coupling to the observable sector only gravitationally. The dark matter density profile ρ(r) = ρ₀/(1+(r/r_c)²) with core radius r_c ≈ 9.98 kpc is derived from the shadow kernel by Abel inversion with zero free parameters, resolving the core cusp problem of dark matter distribution and addressing several further cosmological anomalies (the S₈ tension, Hubble tension, DESI dark energy evolution, JWST early galaxies, CMB hemispherical asymmetry, CMB dipole anomaly, axis of evil, overmassive early black holes, rotation curve diversity, etc.) from a single geometric source. Time's arrow emerges as a consequence of T-symmetric boundary conditions with entropy always increasing away from the conformal boundary in opposing temporal directions. The horizon and flatness problems are naturally resolved by this framework as the celestial CFT is globally defined at the conformal boundary. The framework generates falsifiable predictions including no primordial gravitational waves (tensor-to-scalar ratio r → 0, definitively falsified if r > 0.01 detected by CMB-S4), m_{ν₁} = 0 (KATRIN, JUNO), r_c ≈ 9.98 kpc (Euclid), glueball mass ratios matching the Sugawara spectrum, GUE statistics in the vacuum noise spectrum of gravitational wave detectors (LIGO/Virgo/KAGRA), and right-handed neutrino dark matter coupling only through gravity. Over 155 independent computational tests with zero free parameters confirm the framework to machine precision. Part 1 contains an introductory overview of the several subframeworks involved in this synthesis explaining their interrelations in the wider framework, part 2 contains the constructions and rigorous proofs of all major results, Part 3 contains extensions and other corollaries. Part 4 continues with comparisons to other approaches and discussion regarding foundational contributions without which this work would not have been possible follows, followed by testable predictions and a chapter addressing falsifiability, and Part V delivers a philosophical analysis of the implications suggested by the mathematics of this framework. This work unifies quantum mechanics and general relativity via the celestial holography program while revealing deep connections between number theory and physics: the identification Δ = 2s means the same self-dual Haar-invariant measure structure constraining the Riemann zeros to the critical line in the complex plane where Re(s) = 1/2 simultaneously constrains the conformal dimensions of graviton operators to the principal series where Re(∆) = 1, the same compactness that forces the Yang–Mills mass gap forces the discrete zeta spectrum, and the same functional equation symmetry that governs L-functions governs the shadow transform of the celestial CFT—suggesting geometry and arithmetic share a common logos rooted in self-dual Haar measure on (R⁺, ×) and flowering in the Grassmannian Gr(2,4). (shrink)

The article focuses on process management in public administration using the specific case study of the statutory city of Ostrava. Based on the selected part of the PAPRIS methodology, the process management is verified, and conclusions from the application of information system e-SMO ("Electronic Statutory City of Ostrava") are generalized. Ostrava is third the biggest city in Czech Republic with approximately 320 thousand citizen. Article describes experiences with SW implements, which are used for model of process in public administration. (...) Particulary at local authority of Ostrava town. Model of process is a basis for reengineering of process in state administration and preparation for implementation of big information systems. Mapping of process is providing implement and confirmation methodology to identify existing processes. Problem with its using consist in that, senior manager don’t informs, what organization is determination by processes. If are not described in given to organization current processes, or how would have had look new optimum processes, will not endeavour about reengineering successful. Procedural analysis namely offer tool and check methodology to identification current suit („ at") and it is possible him use either as instruction („ how so about to be") for reengineering function handling administrative and self-rule activities. Purpose of the article: The PAPRIS methodology was used when defining the objectives for implementation of the information system for public administration (PAPRIS - Process Approach - Public and Regional Information System). This methodology has been elaborated by one of the authors and published in a very general scheme when solving many case studies (Krajčík, 2006), (Krajčík, 2007), (Krajčík, 2013) (Krajčík, 2014). We assume that the PAPRIS is primarily a methodology with incorporated elements of procedural approach for project management in public administration information systems (PAIS). The specific supporting process of communication between the client and the e-SMO ("Electronic Statutory City of Ostrava") system has been chosen for verification. The model of supporting communication process, created by ARIS tools, is crucial, and the structure of scripts (ICM and IVR) is subsequently made. The aim of this article is to verify that the methodology is sufficient and appropriate to manage such a large project such, undoubtedly, is the e-SMO (Vlček, 2009). Methodology/methods: Defined productive and non-productive processes with their defined process cuts represent a crucial category for the process structure of IS projects. This is fully accepted by the PAPRIS methodology. Process cuts are understood, in the logic modelling according to the PAPRIS methodology, as clearly defined logic directional cuts in three-dimensional space of all project processes. The process set is systemically categorized, in a given logic directional cut, into mutually disjoint process subsets, which are characterized by this particular directional operator. The directional operator always has a clear logical allocation that is based on the construction of a process view. Theoretically, an infinite number of process views can be used. One of the important issues in a methodology for the case studies includes the size of the research sample. It is usually assumed that there is no ideal number of cases and that the number between four and ten usually provides good results. Other authors defining against any quantitative standards for any determination of the sample size of the case studies, since such an approach denies the internal logic of this methodology and the richness of the information obtained from participants in the research. Research which is carried out using case studies does not aspire on compliance with the requirement the representativeness of the sample. (Štrach, 2007). Methodology of case studies is among the established guidelines of qualitative research (Štrach, 2007). Research on using case studies in the last 30 years has seen an extraordinary increase in social-scientific research, including research on business and management (Dul, Hak, 2008). Scientific aim: The essential aim of this study is to describe the way the process cut defines a productive process and non-productive process, in accordance with the PAPRIS methodology using the specific example. While the triggering mechanism of the project production process is an event causing its own production - i.e. the specific output with added value for the customer, the project of non-productive process is caused by the project management event. Therefore, it is caused by the need to control, monitor, track, inspect, evaluate outputs, decide and regulate the project implementation. Findings: Within the support of the communication process, two examples were used to verify the methodology. The global perspective on the process was created in ARIS tools and the communication between the call centre and the client was made in Visio tools. The PAPRIS methodology is based on the concept of process variability, which has been clearly formulated. The fundamental direction of the process development, anticipated changes and the opportunity to react to them in accordance with defined objectives of the PAIS project are guaranteed. (shrink)