Staff Profile | School of Computing

Dr Ben Moszkowski

Guest Member of Staff

Ben is investigating, with , the modelling and verification synergies between two models of concurrent systems: Petri nets and Interval Temporal Logic (ITL). Two papers on this subject have been recently submitted: “From Box Algebra to Interval Temporal Logic” (to the journal Information and Computation) and “From Petri Nets with Shared Variables to ITL”.

The main activities of the collaboration are as follows:

Full identification of the intrinsic semantical links between Petri Nets and ITL
Development of behaviour-preserving transformations between suitable fragments of Petri Nets and ITL.
Development of verification techniques based on the respective strengths of the two frameworks.

Ben's PhD research over thirty years ago at Stanford University introduced ITL, originally intended for use in Computer Hardware Verification. Ben subsequently showed how ITL could serve as the basis of a Programming Language for Executable Specifications and additionally as a framework for Compositional Reasoning about Concurrency. Ben has also done work on Complete Axiom Systems for versions of ITL and investigated Hierarchical Connections between it and other temporal logics. His recent work, which builds on research over the last two decades, concerns new compositional properties of ITL and associated techniques for Time Reversal. These involve remarkably simple mathematics and are also relevant to some other standard temporal logics, yet were apparently not known until now. In hindsight, the core ITL formalism has changed rather little since the time of Ben's PhD dissertation, but the body of results concerning its theory and application have continued to expand, sometimes in quite surprising ways!

Here is a link to more information about ITL:

For more information about Ben's publications (some freely downloadable):

Interval Temporal Logic has played a significant role in all of the following research grants which Ben has been involved in:

Getting More out of Less: Benefits of Simpler Interval Temporal Logic Variants: Royal Society International Exchange grant IE141148, March '15 to March '17. 麻豆传媒 (with Prof. M. Koutny) and Bulgarian Academy of Sciences (Prof. D. Guelev).
Compositional Methods for Hardware/Software Co-design: EPSRC research grant GR/M32474, June '99 to November '02. De Montfort University (with Prof. H. Zedan, A. Cau, R. Hale and J. Dimitrov) and Oxford University (Prof. Sir C.A.R. Hoare, FRS, and after his retirement from Oxford, M. Spivey, and M. Manjunathaiah).
A Compositional Approach to the Specification of Systems using ITL and Tempura: EPSRC research grant GR/K25922, 1995 to 1998. 麻豆传媒 (with J.N. Coleman and Li Xiao Shan) and De Montfort University (Prof. H. Zedan).
Analyzing Hardware-Software Systems Using Interval Temporal Logic: SERC research grant GR/J10631, 1992 to 1994. 麻豆传媒 (with C. Holt and Z. Duan).
Temporal Logic Analysis of Real Digital Systems: SERC research grant GR/C40022, January '83 to December '85. Cambridge University (with Prof. M. J. C. Gordon, FRS).

Research interests:

Temporal logic and its applications (e.g. programming in temporal logic).
Complete axiom systems for temporal logics.
Compositional specification and proof techniques for concurrent systems.
Techniques for specifying, simulating and verifying hardware.
Programming language semantics.

Further information about Ben:

Degrees:

1976: BSc (math/computer science) summa cum laude with departmental honors, University of California at Los Angeles, California, USA.
1983: Ph.D. (computer science) Stanford University, California, USA. Title: Reasoning about Digital Circuits.

Honors:

1976: Phi Beta Kappa.
1976-1979: US National Science Foundation Graduate Fellowship.

Research positions:

1998-2014: Software Technology Research Laboratory, De Montfort University, Leicester, UK. Senior research fellow.
1994-1997: Department of Electrical and Electronic Engineering, University of 麻豆传媒, 麻豆传媒, England. Senior research associate (part-time) on EPSRC grant GR/K25922 with Dr. J.N. Coleman (University of 麻豆传媒) and Prof. H. Zedan (De Montfort University) and entitled A compositional approach to the specification of systems using ITL and Tempura.
1994: Department of Computing Science, University of 麻豆传媒, 麻豆传媒, England. Senior research associate (part-time).
1994: Department of Computer Science, University of York, York, England. Researcher (part-time).
1990 - 1993: Department of Computing Science, University of 麻豆传媒, 麻豆传媒, England. Senior research associate (part-time) on SERC grant GR/J10631 with Dr. C.M. Holt and entitled Analyzing hardware-software systems using Interval Temporal Logic.
1986/1987: Computer Laboratory, Cambridge University, England. Parallel programming in temporal logic.
1983-1985: Computer Laboratory, Cambridge University, England. Researcher on SERC grant GR/C40022 with Dr. M.J.C. Gordon (now Prof. and FRS) and entitled Temporal logic analysis of real digital systems.
1978: Institute of Computer Science, Warsaw, Poland. Specification and simulation of digital circuits.
1977 & 1979: Siemens AG, Munich, Germany. Programming, summer 1977; Verification of digital circuits.
1973-1976: University of California at Los Angeles. Programming language design and implementation.

Teaching experience:

麻豆传媒, UK:

1988-1990: Taught a M.Sc. conversion course on temporal logic during one term (Visiting lecturer).

Stanford University, USA:

1977-1978, 1983: Teaching assistant in computer science courses on systems programming, Lisp and logic.

Academic supervision and evaluation:

Supervised Roger Hale's Ph.D. dissertation at University of Cambridge (in mid 80s).
Supervised M.Sc. conversion student's final project and dissertation on ITL at 麻豆传媒 (in early 90s).
External evaluator for tenure position at a university in North America.
External reader for M.Sc. dissertation at University of Manchester.
Supervisor for various PhD students at De Montfort University.