The Calculus of Temporal Influence

Bruse, Florian; Kastaun, Marit; Lange, Martin; Möller, Sören

doi:10.4230/LIPIcs.TIME.2023.10

File

LIPIcs.TIME.2023.10.pdf

Filesize: 0.73 MB
19 pages

Document Identifiers

DOI: 10.4230/LIPIcs.TIME.2023.10
URN: urn:nbn:de:0030-drops-191009

Author Details

Florian Bruse

Theoretical Computer Science / Formal Methods, University of Kassel, Germany

Marit Kastaun

Didactics of Biology, University of Kassel, Germany

Martin Lange

Theoretical Computer Science / Formal Methods, University of Kassel, Germany

Sören Möller

Theoretical Computer Science / Formal Methods, University of Kassel, Germany

Cite AsGet BibTex

Florian Bruse, Marit Kastaun, Martin Lange, and Sören Möller. The Calculus of Temporal Influence. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TIME.2023.10

Abstract

We present the Calculus of Temporal Influence, a simple logical calculus that allows reasoning about the behaviour of real-valued functions over time by making assertions that bound their values or the values of their derivatives. The motivation for the design of such a proof system comes from the need to provide the background computational machinery for tools that support learning in experimental subjects in secondary-education classrooms. The end goal is a tool that allows school pupils to formalise hypotheses about phenomena in natural sciences, such that their validity with respect to some formal experiment model can be checked automatically. The Calculus of Temporal Influence provides a language for formal statements and the mechanisms for reasoning about valid logical consequences. It extends (and deviates in parts from) previous work introducing the Calculus of (Non-Temporal) Influence by integrating the ability to model temporal effects in such experiments. We show that reasoning in the calculus is sound with respect to a natural formal semantics, that logical consequence is at least semi-decidable, and that one obtains polynomial-time decidability for a natural stratification of the problem.

Subject Classification

ACM Subject Classification

Theory of computation → Theory and algorithms for application domains
Theory of computation → Automated reasoning
Applied computing → Interactive learning environments

Keywords

temporal reasoning
formal models
continuous functions
polynomial decidability

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

R. Alur, C. Belta, F. Ivančić, V. Kumar, M. Mintz, G. J. Pappas, H. Rubin, and J. Schug. Hybrid modeling and simulation of biomolecular networks. In Proc. 4th Int. Workshop on Hybrid Systems: Computation and Control, HSCC'01, volume 2034 of LNCS, pages 19-32, 2001.
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
J. Arias, M. Carro, Z. Chen, and G. Gupta. Modeling and reasoning in event calculus using goal-directed constraint answer set programming. Theory Pract. Log. Program., 22(1):51-80, 2022. URL: https://doi.org/10.1017/S1471068421000156.
F. Bruse, M. Lange, and S. Möller. Formal reasoning about influence in natural sciences experiments. In Proc. 29th Int. Conf. on Computed-Aided Deduction, CADE'23, LNAI. Springer, 2023. To appear.
C. Chaouiya. Petri net modelling of biological networks. Briefings in Bioinformatics, 8(4):210-219, 2007.
T. de Jong. Moving towards engaged learning in stem domains; there is no simple answer, but clearly a road ahead. Journal of Computer Assisted Learning, 35(2):153-167, 2019. URL: https://doi.org/10.1111/jcal.12337.
T. A. Henzinger. The theory of hybrid automata. In Proc. 11th Annual IEEE Symp. on Logic in Computer Science, pages 278-292. IEEE, 1996.
T. Irion and K. Scheiter. Didaktische Potenziale digitaler Medien. Der Einsatz digitaler Technologien aus grundschul- und mediendidaktischer Sicht. Grundschule aktuell, 142:8-11, 2018.
M. Kastaun, M. Meier, N. Hundeshagen, and M. Lange. ProfiLL: Professionalisierung durch intelligente Lehr-Lernsysteme. In Bildung, Schule, Digitalisierung, pages 357-363. Waxmann-Verlag, 2020.
I. Koch. Petri nets – a mathematical formalism to analyze chemical reaction networks. Molecular Informatics, 29(12):838-843, 2010. URL: https://doi.org/10.1002/minf.201000086.
OECD. PISA 2006 - Science Competencies for Tomorrow’s World: Volume 1: Analysis. OECD Publishing, 2007. URL: https://doi.org/10.1787/9789264040014-en.
R. S. Palais and R. A. Palais. Differential Equations, Mechanics, and Computation, volume 51 of Student mathematical library; IAS/Park City mathematical subseries. AMS, 2009.
L. Popova-Zeugmann. Timed Petri Nets, pages 139-172. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-41115-1_4.
L. J. Steggles, R. Banks, and A. Wipat. Modelling and analysing genetic networks: From boolean networks to petri nets. In International conference on computational methods in systems biology, pages 127-141. Springer, 2006.
G. Theocharopoulou, C. Bobori, and P. Vlamos. Formal models of biological systems. In Proc. 2nd World Congress on Genetics, Geriatrics and Neurodegenerative Disease, GeNeDis'16, pages 325-338. Springer, 2017.