5.1 Articles

[1]

Dimitar P. Guelev and Ben Moszkowski. “Expressive completeness by separation for discrete time interval temporal logic with expanding modalities”. In: Information Processing Letters 186 (2024), p. 106480. issn: 0020-0190.
url: https://www.sciencedirect.com/science/article/pii/S0020019024000103.

[2]

Dimitar P. Guelev and Ben Moszkowski. “A separation theorem for discrete-time interval temporal logic”. In: Journal of Applied Non-Classical Logics 32.1 (2022), pp. 28–54.
url: https://doi.org/10.1080/11663081.2022.2050135.

[3]

Hanna Klaudel, Maciej Koutny, Zhenhua Duan, and Ben Moszkowski. “From Box Algebra to Interval Temporal Logic”. In: Fundamenta Informaticae 167.4 (2019), pp. 323–354.
url: http://dx.doi.org/10.3233/FI-2019-1820.

[4]

Ben Moszkowski and Dimitar Guelev. “An application of temporal projection to interleaving concurrency”. In: Formal Aspects of Computing 29.4 (July 2017), pp. 705–750.
url: http://dx.doi.org/10.1007/s00165-017-0417-3.

[5]

Brijesh Dongol, Ian J. Hayes, and Georg Struth. “Convolution As a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency”. In: ACM Trans. Comput. Logic 17.3 (Feb. 2016), 15:1–15:25. issn: 1529-3785.
url: http://doi.acm.org/10.1145/2874773.

[6]

Stéphane Demri and Morgan Deters. “Two-Variable Separation Logic and Its Inner Circle”. In: ACM Trans. Comput. Logic 16.2 (Apr. 2015), 15:1–15:36. issn: 1529-3785.
url: http://dx.doi.org/10.1145/2724711.

[7]

Helge Janicke, Andrew Nicholson, Stuart Webber, and Antonio Cau. “Runtime-Monitoring for Industrial Control Systems”. In: Electronics 4.4 (Dec. 2015). Ed. by Dhananjay Phatak. Open Access, pp. 995–1017.
url: http://dx.doi.org/10.3390/electronics4040995.

[8]

Qian Ma, Zhenhua Duan, Nan Zhang, and Xiaobing Wang. “Verification of distributed systems with the axiomatic system of MSVL”. In: Formal Aspects of Computing 27.1 (2015), pp. 103–131. issn: 0934-5043.
url: http://dx.doi.org/10.1007/s00165-014-0303-1.

[9]

Ben Moszkowski. “Compositional reasoning using intervals and time reversal”. In: Annals of Mathematics and Artificial Intelligence 71.1-3 (2014), pp. 175–250. issn: 1012-2443.
url: http://dx.doi.org/10.1007/s10472-013-9356-8.

[10]

Ben Moszkowski, Dimitar Guelev, and Martin Leucker. “Guest editors’ preface to special issue on interval temporal logics”. In: Ann. Math. Artif. Intell. 71.1-3 (2014), pp. 1–9.
url: http://dx.doi.org/10.1007/s10472-014-9417-7.

[11]

Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Jörg Pfähler, and Wolfgang Reif. “RGITL: A temporal logic framework for compositional reasoning about interleaved programs”. In: Annals of Mathematics and Artificial Intelligence 71.1-3 (2014), pp. 131–174. issn: 1012-2443.
url: http://dx.doi.org/10.1007/s10472-013-9389-z.

[12]

Bogdan Tofan, Oleg Travkin, Gerhard Schellhorn, and Heike Wehrheim. “Two approaches for proving linearizability of multiset”. In: Science of Computer Programming 96, Part 3.0 (2014), pp. 297–314. issn: 0167-6423.
url: http://dx.doi.org/10.1016/j.scico.2014.04.001.

[13]

Alasdair Armstrong, Georg Struth, and Tjark Weber. “Kleene Algebra”. In: Archive of Formal Proofs (2013). http://isa-afp.org/entries/Kleene_Algebra.shtml, Formal proof development. issn: 2150-914x.

[14]

Antonio Cau, Helge Janicke, and Ben Moszkowski. “Verification and enforcement of access control policies”. In: Formal Methods in System Design 43.3 (2013). Download pdf, pp. 450–492. issn: 0925-9856.
url: http://dx.doi.org/10.1007/s10703-013-0187-3.

[15]

Zhenhua Duan, Hanna Klaudel, and Maciej Koutny. “ITL semantics of composite Petri nets”. In: The Journal of Logic and Algebraic Programming 82.2 (2013), pp. 95–110. issn: 1567-8326.
url: http://dx.doi.org/10.1016/j.jlap.2012.12.001.

[16]

Zhenhua Duan, Nan Zhang, and Maciej Koutny. “A complete proof system for propositional projection temporal logic”. In: Theoretical Computer Science 497.0 (2013), pp. 84–107. issn: 0304-3975.
url: http://dx.doi.org/10.1016/j.tcs.2012.01.026.

[17]

Helge Janicke, Antonio Cau, François Siewe, and Hussein Zedan. “Dynamic Access Control Policies: Specification and Verification”. In: The Computer Journal 56.4 (2013). Download pdf, pp. 440–463.
url: http://dx.doi.org/10.1093/comjnl/bxs102.

[18]

Ben Moszkowski. “Interconnections between classes of sequentially compositional temporal formulas”. In: Information Processing Letters 113.9 (2013), pp. 350–353. issn: 0020-0190.
url: http://dx.doi.org/10.1016/j.ipl.2013.02.005.

[19]

Nan Zhang, Zhenhua Duan, and Cong Tian. “A cylinder computation model for many-core parallel computing”. In: Theoretical Computer Science 497.0 (2013), pp. 68–83. issn: 0304-3975.
url: http://dx.doi.org/10.1016/j.tcs.2012.02.011.

[20]

Sulaiman Al Amro and Antonio Cau. “Behavioural API based Virus Analysis and Detection”. In: International Journal of Computer Science and Information Security 10.5 (May 2012). Download pdf, pp. 14–22.
url: https://sites.google.com/site/ijcsis/vol-10-no-5-may-2012.

[21]

Ben C. Moszkowski. “A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time”. In: Logical Methods in Computer Science Journal 8.3 (2012).
url: http://dx.doi.org/10.2168/LMCS-8(3:10)2012.

[22]

Turki Alghamdi, Hussein Zedan, and Ali Alzahrani. “Enforcing Learning Activities Policies in Runtime Monitoring System for E-learning Environments”. In: International Journal of Computer Science and Information Security (IJCSIS) 9.8 (2011), pp. 45–53.
url: https://sites.google.com/site/ijcsis/vol-9-no-8-aug-2011.

[23]

Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan, and Wolfgang Reif. “Proving linearizability with temporal logic”. In: Formal Aspects of Computing 23.1 (2011), pp. 91–112. issn: 0934-5043.
url: http://dx.doi.org/10.1007/s00165-009-0130-y.

[24]

Gudmund Grov and Stephan Merz. “A Definitional Encoding of TLA∗ in Isabelle/HOL”. In: Archive of Formal Proofs (2011). https://www.isa-afp.org/entries/TLA.html, Formal proof development. issn: 2150-914x.

[25]

Alan Burns and Ian J. Hayes. “A timeband framework for modelling real-time systems”. In: Real-Time Systems 45.1-2 (2010), pp. 106–142. issn: 0922-6443.
url: http://dx.doi.org/10.1007/s11241-010-9094-5.

[26]

Andreas Lochbihler. “Coinductive”. In: Archive of Formal Proofs (2010). https://www.isa-afp.org/entries/Coinductive.html, Formal proof development. issn: 2150-914x.

[27]

Ben Moszkowski. “Using Temporal Logic to Analyse Temporal Logic: A Hierarchical Approach Based on Intervals”. In: Journal of Logic and Computation 17.2 (2007). Download pdf, pp. 333–409.
url: http://dx.doi.org/10.1093/logcom/exm006.

[28]

Dimitar P. Guelev and Dang Van Hung. “On the Completeness and Decidability of Duration Calculus with Iteration”. In: Theoretical Computer Science 337 (2005), pp. 278–304.
url: http://dx.doi.org/10.1016/j.tcs.2005.01.017.

[29]

Shikun Zhou, Hussein Zedan, and Antonio Cau. “Run-time Analysis of Time-critical Systems”. In: Journal of System Architecture 51.5 (2005). Download pdf, pp. 331–345.
url: http://dx.doi.org/10.1016/j.sysarc.2004.12.003.

[30]

Zhen-Hua Duan and Maciej Koutny. “A framed temporal logic programming language”. In: Journal of Computer Science and Technology 19.3 (2004), pp. 341–351. issn: 1000-9000.
url: http://dx.doi.org/10.1007/BF02944904.

[31]

Rodolfo Gomez and Howard Bowman. “PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic”. In: Journal of Applied Non-Classical Logics 14.1–2 (2004), pp. 105–148.
url: http://dx.doi.org/10.3166/jancl.14.105-148.

[32]

Wang Hanpin and Xu Qiwen. “Completeness of temporal logics over infinite intervals”. In: Discrete Applied Mathematics 136.1 (2004). Discrete Mathematics and Theoretical Computer Science (DMTCS), pp. 87–103. issn: 0166-218X.
url: http://dx.doi.org/10.1016/S0166-218X(03)00201-4.

[33]

Ben Moszkowski. “A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time”. In: Journal of Applied Non-Classical Logics 14.1–2 (2004), pp. 55–104.
url: http://dx.doi.org/10.3166/jancl.14.55-104.

[34]

Howard Bowman and Simon J. Thompson. “A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection”. In: Journal of Logic and Computation 13.2 (Apr. 2003), pp. 195–239.
url: http://dx.doi.org/10.1093/logcom/13.2.195.

[35]

Antonio Cau et al. “A Compositional Framework for Hardware/Software Co-Design”. In: Design Automation for Embedded Systems 6.4 (2002). Ed. by Raul Camposano, Wayne Wolf, and Bashir Al-Hashimi. Download pdf, pp. 367–399. issn: 0929-5585.
url: http://dx.doi.org/10.1023/A:1016507527035.

[36]

R. Mattolini and P. Nesi. “An Interval Logic for Real-Time System Specification”. In: Transactions on Software Engineering, IEEE 27.3 (Mar. 2001), pp. 208–227.
url: http://dx.doi.org/10.1109/32.910858.

[37]

Hongji Yang, Xiaodong Liu, and Hussein Zedan. “Abstraction: A Key Notion for Reverse Engineering in A Reengineering Approach”. In: Journal of Software Maintenance: Research and Practice 12.4 (2000), pp. 197–228.
url: http://dx.doi.org/10.1002/1096-908X(200007/08)12:4%3C197::AID-SMR211%3E3.0.CO;2-X.

[38]

Zhiqiang Chen, Hussein Zedan, Antonio Cau, and Hongji Yang. “A Wide-Spectrum Language for Object-Based Development of Real-time Systems”. In: Journal of Information Sciences 118 (1999). Download pdf, pp. 15–35.
url: http://dx.doi.org/10.1016/S0020-0255(99)00039-0.

[39]

Hussein Zedan, Antonio Cau, Zhiqiang Chen, and Hongji Yang. “ATOM: An Object-based Formal Method for Real-time Systems”. In: Annals of Software Engineering 7 (1999). Download pdf, pp. 235–256.
url: http://dx.doi.org/10.1023/A:1018942406449.

[40]

Ben Moszkowski. “Executable Temporal Logic Systems: The programming language Tempura”. In: Journal of Symbolic Computation 22.5-6 (1996). Download pdf, pp. 730–733. issn: 0747-7171.
url: http://dx.doi.org/10.1006/jsco.1996.0073.

[41]

Y. Srinivas Ramakrishna, Peter M. Melliar-Smith, Louise E. Moser, Laura K. Dillon, and George Kutty. “Interval logics and their decision procedures. Part II: A real-time interval logic”. In: Theoretical Computer Science 170.1–2 (Dec. 1996), pp. 1–46.
url: http://dx.doi.org/10.1016/S0304-3975(96)80701-8.

[42]

Y. Srivinas Ramakrishna, Peter M. Melliar-Smith, Louise E. Moser, Laura K. Dillon, and George Kutty. “Interval logics and their decision procedures. Part I: An interval logic”. In: Theoretical Computer Science 166.1–2 (Oct. 1996), pp. 1–47.
url: http://dx.doi.org/10.1016/0304-3975(95)00254-5.

[43]

Laura K. Dillon, George Kutty, Louise E. Moser, Peter M. Melliar-Smith, and Y. Srinivas Ramakrishna. “A Graphical Interval Logic for Specifying Concurrent Systems”. In: ACM Transactions on Software Engineering and Methodology 3.2 (Apr. 1994), pp. 131–165.
url: http://dx.doi.org/10.1145/192218.192226.

[44]

R. Dowsing, E. Elliot, and I. Marshall. “Automated technique for high-level circuit synthesis from temporal logic specifications”. In: IEE Proceedings–Computers and Digital Techniques 141.3 (May 1994), pp. 145–152.
url: http://dx.doi.org/10.1049/ip-cdt:19941005.

[45]

Michael R. Hansen. “Model-Checking Discrete Duration Calculus”. In: Formal Aspects of Computing 6.1 (1994), pp. 826–845.
url: http://dx.doi.org/10.1007/BF01213605.

[46]

Masahiro Fujita and Shinji Kono. “Synthesis of Controllers from Interval Temporal Logic Specification”. In: International Workshop on Logic Synthesis (1993).

[47]

Kiyoharu Hamaguchi, Hiromi Hiraishi, and Shuzo Yajima. “Infinity-Regular Temporal Logic and its Model Checking Problem”. In: Theor. Comput. Sci. 103.2 (1992), pp. 191–204.
url: http://dx.doi.org/10.1016/0304-3975(92)90012-5.

[48]

Hiromi Hiraishi, Kiyoharu Hamaguchi, Hiroshi Fujii, and Shuzo Yajima. “Regular Temporal Logic Expressively Equivalent to Finite Automata and its Application to Logic Design Verification”. In: Journal of Information Processing 15.1 (1992), pp. 129–138.
url: http://ci.nii.ac.jp/naid/110002673621/en/.

[49]

Joseph Y. Halpern and Yoav Shoham. “A propositional modal logic of time intervals”. In: J. ACM 38.4 (Oct. 1991), pp. 935–962. issn: 0004-5411. doi: 10.1145/115234.115351.
url: https://doi.org/10.1145/115234.115351.

[50]

Antonio Nunez, Don Fay, R.D. Dowsing, and R. Elliott. “A higher level of behavioural specification: An example in Interval Temporal Logic”. In: Microprocessing and Microprogramming 32.1 (1991), pp. 517–524. issn: 0165-6074.
url: http://dx.doi.org/10.1016/0165-6074(91)90395-A.

[51]

Yde Venema. “A Modal Logic for Chopping Intervals”. In: Journal of Logic and Computation 1.4 (Sept. 1991), pp. 453–476. issn: 0955-792X. doi: 10.1093/logcom/1.4.453. eprint: https://academic.oup.com/logcom/article-pdf/1/4/453/3817096/1-4-453.pdf.
url: https://doi.org/10.1093/logcom/1.4.453.

[52]

Chaochen Zhou, Charles Antony Richard Hoare, and Anders P. Ravn. “A Calculus of Durations”. In: Information Processing Letters 40.5 (1991), pp. 269–276.
url: http://dx.doi.org/10.1016/0020-0190(91)90122-X.

[53]

Miriam Leeser. “Reasoning About the Function and Timing of Integrated Circuits with Interval Temporal Logic”. In: IEEE Transactions on Computer-Aided Design 8.12 (Dec. 1989), pp. 1233–1246.
url: http://dx.doi.org/10.1109/43.44505.

[54]

Masahiro Fujita, Shinji Kono, Hidehiko Tanaka, and Tatsuhiko Moto-Oka. “Aid to hierarchial and structured logic design using temporal logic and Prolog”. In: IEE Proceedings E (Computers and Digital Techniques) 133 (5 Sept. 1986), pp. 283–294. issn: 0143-7062.
url: http://dx.doi.org/10.1049/ip-e.1986.0035.

[55]

Ben Moszkowski. “A Temporal Logic for Multilevel Reasoning about Hardware”. In: IEEE Computer 18.2 (1985), pp. 10–19. issn: 0018-9162.
url: http://dx.doi.org/10.1109/MC.1985.1662795.

[56]

James F. Allen. “Maintaining Knowledge about Temporal Intervals”. In: Commun. ACM 26.11 (Nov. 1983), pp. 832–843. issn: 0001-0782.
url: https://doi.org/10.1145/182.358434.