pith. sign in

arxiv: 2401.01884 · v3 · submitted 2024-01-03 · 💻 cs.LO

A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets

Jaime Arias , Kyungmin Bae , Carlos Olarte , Peter Csaba \"Olveczky , Laure Petrucci This is my paper

Pith reviewed 2026-05-24 04:16 UTC · model grok-4.3

classification 💻 cs.LO
keywords parametric time Petri netsrewriting logicSMT solvingparameter synthesisformal verificationbisimulationreachability analysisLTL model checking
0
0 comments X

The pith

A bisimilar rewriting-logic semantics for parametric time Petri nets enables sound and complete analysis plus parameter synthesis inside Maude with SMT solvers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines both a concrete and a symbolic rewriting-logic semantics for parametric time Petri nets that include inhibitor arcs and parameters in firing bounds. It proves these semantics are bisimilar to the accepted standard semantics of such nets. Because of the bisimulation, any reachability or LTL result obtained in Maude with SMT solvers transfers directly back to the original net without loss of soundness or completeness. A new general folding technique for symbolic states guarantees that the Maude analysis terminates exactly when the net's parametric state-class graph is finite. The same encoding also supports synthesis from parametric initial markings and user-defined execution strategies, reproducing nearly all features of the Romeo tool while adding LTL model checking.

Core claim

The authors construct concrete and symbolic rewriting-logic semantics for PITPNs, prove bisimilarity to the standard semantics, and introduce a folding method for symbolic reachability so that Maude-with-SMT analyses are sound, complete, and terminating on finite state-class graphs; this encoding transfers all supported Romeo analyses plus full LTL checking and strategy-based exploration to the Maude framework.

What carries the argument

The bisimilar rewriting-logic semantics for PITPNs, which transfers verification properties from Maude to the original model via equivalence.

If this is right

  • Reachability and parameter synthesis queries on PITPNs become executable inside Maude whenever the parametric state-class graph is finite.
  • Full LTL model checking and analysis under user-defined execution strategies become available for these nets.
  • Parameter synthesis is possible even when initial markings contain parameters.
  • Almost every analysis method previously available only in Romeo can now be performed inside the Maude environment.
  • The Maude implementation outperforms Romeo on many benchmark instances.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same bisimulation technique could be reused to import other Maude capabilities, such as statistical model checking, into the PITPN setting.
  • The folding approach may generalize to other parametric timed formalisms whose state-class graphs admit finite representations.
  • User-defined strategies in Maude could be employed to prune exploration in very large parametric nets before full state-class construction.

Load-bearing premise

Bisimilarity between the rewriting-logic encoding and the standard PITPN semantics is enough to preserve every property needed for reachability, LTL satisfaction, and parameter synthesis.

What would settle it

A concrete PITPN example on which Maude with SMT reports a reachable marking or a synthesized parameter interval that differs from the result of the standard parametric state-class graph algorithm.

Figures

Figures reproduced from arXiv: 2401.01884 by Carlos Olarte, Jaime Arias, Kyungmin Bae, Laure Petrucci, Peter Csaba \"Olveczky.

Figure 1
Figure 1. Figure 1: A PITPN and its valuation. A transition firing interval endpoint should typically either be a non-negative rational number, the infinity value ∞, or a single parameter [3]. However, for convenience we also allow more complex endpoints as e.g., [2a, 2a] where a is a parameter (see [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A simple production-consumption system taken from [42]. The term net3(l,u) represents an instance of a more general version of the net in [PITH_FULL_IMAGE:figures/full_fig_p018_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The scheduling case study taken from [46]. values of the parameter a making the net 1-safe, subject to initial constraint ϕ = 30 ≤ a ≤ 70. The same query can be answered in Maude: Maude> red AG-synthesis in ’MODEL : (net, m0, ϕ) s.t. k-bounded(1) . result BoolExpr: 48 < rr("A") and rr("A") <= 70 The first counterexample found assumes that a ≤ 48. If a > 48, folding does not find any state not satisfying k-… view at source ↗
Figure 4
Figure 4. Figure 4: The tutorial case study. Example 6.4. Consider the PITPN tutorial in [PITH_FULL_IMAGE:figures/full_fig_p035_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: EF-Synthesis. Execution times in log-scale for Roméo and Maude connected with Yices2 (#), Maude-SE with Yices2 (⋆), Z3 (□), and CVC4 (♢). reduction of the search space (folding states in different branches of the search tree) allows folding to solve some instances faster in the scheduling benchmark (see the three items on the right in Fig. 8b). We have also compared the performance of the folding analysis … view at source ↗
Figure 6
Figure 6. Figure 6: EF-Synthesis. Execution times in log-scale for Roméo and Maude connected with Yices2 (#), Maude-SE with Yices2 (⋆), Z3 (□), and CVC4 (♢) [PITH_FULL_IMAGE:figures/full_fig_p041_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: AG-Synthesis. Execution times in log-scale for Roméo and Maude connected with Yices2 (#), Maude-SE with Yices2 (⋆), Z3 (□), and CVC4 (♢) [PITH_FULL_IMAGE:figures/full_fig_p042_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Comparison of the different Maude commands in log-scale. Maude with Yices2 ( [PITH_FULL_IMAGE:figures/full_fig_p043_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Comparison of the implementation reported in this paper and the one in [35]. [PITH_FULL_IMAGE:figures/full_fig_p044_9.png] view at source ↗
read the original abstract

This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the "standard" semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude -- including full LTL model checking, analysis with user-defined analysis strategies, and even statistical model checking -- for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Romeo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Romeo in many cases.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The manuscript presents concrete and symbolic rewriting-logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs). It asserts a bisimulation proof between these semantics and the standard PITPN state-class semantics. This is used to justify employing Maude combined with SMT solving for sound and complete analyses (reachability, LTL model checking, parameter synthesis), including from parametric initial markings. A new general folding operator for symbolic reachability is introduced so that analysis terminates whenever the underlying parametric state-class graph is finite. The work claims to replicate nearly all Romeo analyses while adding LTL, user-defined strategies, and statistical model checking, with experiments indicating outperformance over Romeo in many cases.

Significance. If the bisimulation is a strong relation that exactly preserves enabledness, firing intervals, and symbolic parameter constraints, and if the folding operator is proven to preserve LTL obligations, the result would allow Maude's full suite of analyses to be applied soundly to PITPNs. This would be a useful addition to the parametric timed-systems verification toolbox, particularly for the added support of parametric initial markings and custom execution strategies.

major comments (3)
  1. [Abstract and §4] Abstract and §4 (Bisimilarity): the central claim that the Maude encoding is bisimilar to the standard PITPN semantics (and therefore transfers soundness and completeness for LTL and parametric synthesis) is asserted without any proof sketch, key lemmas, or explicit definition of the bisimulation relation; this prevents verification that the relation is strong and handles inhibitor arcs plus parametric initial markings without precision loss.
  2. [§5] §5 (Folding approach): the new general folding operator is claimed to guarantee termination precisely when the parametric state-class graph is finite and to preserve reachability; however, neither the formal definition of the operator nor the argument that it does not merge states differing on future LTL obligations is supplied, which is load-bearing for the completeness claim.
  3. [§6] §6 (Experiments): the reported outperformance over Romeo is stated without benchmark descriptions, instance sizes, or raw metrics (e.g., number of states explored, synthesis times), making it impossible to assess whether the folding and SMT encoding deliver the claimed gains on the same problems.
minor comments (2)
  1. [§3] Notation for parametric constraints and state-class representations should be introduced once and used consistently across the semantics and folding sections.
  2. A short comparison table listing which Romeo features are reproduced and which additional Maude features are newly supported would improve readability.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the detailed and constructive report. We address each major comment below and will strengthen the manuscript accordingly.

read point-by-point responses

  1. Referee: [Abstract and §4] Abstract and §4 (Bisimilarity): the central claim that the Maude encoding is bisimilar to the standard PITPN semantics (and therefore transfers soundness and completeness for LTL and parametric synthesis) is asserted without any proof sketch, key lemmas, or explicit definition of the bisimulation relation; this prevents verification that the relation is strong and handles inhibitor arcs plus parametric initial markings without precision loss.

    Authors: We agree that an explicit definition of the bisimulation relation together with a proof sketch and key lemmas is needed in §4 to make the strength of the relation and its handling of inhibitor arcs and parametric initial markings fully verifiable. We will add these elements in the revision. revision: yes

  2. Referee: [§5] §5 (Folding approach): the new general folding operator is claimed to guarantee termination precisely when the parametric state-class graph is finite and to preserve reachability; however, neither the formal definition of the operator nor the argument that it does not merge states differing on future LTL obligations is supplied, which is load-bearing for the completeness claim.

    Authors: We acknowledge that the formal definition of the folding operator and the argument establishing that it preserves LTL obligations (by not merging states with differing future behaviors) must be supplied. We will include both in the revised §5. revision: yes

  3. Referee: [§6] §6 (Experiments): the reported outperformance over Romeo is stated without benchmark descriptions, instance sizes, or raw metrics (e.g., number of states explored, synthesis times), making it impossible to assess whether the folding and SMT encoding deliver the claimed gains on the same problems.

    Authors: We will expand §6 with benchmark descriptions, instance sizes, and raw metrics (states explored, synthesis times) so that the performance comparison can be assessed directly. revision: yes

Circularity Check

0 steps flagged

No circularity: bisimilarity is a new proof to external standard semantics

full rationale

The paper constructs a rewriting-logic semantics for PITPNs, states a bisimilarity theorem to the independently defined standard state-class semantics of PITPNs, and uses that theorem to justify Maude+SMT analyses. No equation, definition, or claim reduces a derived result to its own inputs by construction; the bisimulation is not obtained by fitting, renaming, or self-citation load-bearing. The derivation chain therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on standard properties of rewriting logic, bisimulation, and SMT solvers; the main additions are the concrete PITPN encoding and the folding operator.

axioms (2)
  • domain assumption Bisimilarity between the Maude semantics and the standard PITPN semantics preserves reachability, LTL properties, and parameter synthesis results.
    Invoked to claim soundness and completeness of all analyses performed in Maude.
  • domain assumption The parametric state-class graph being finite is a sufficient condition for termination of the symbolic reachability procedure.
    Directly stated as the termination condition for the new folding approach.

pith-pipeline@v0.9.0 · 5765 in / 1474 out tokens · 35308 ms · 2026-05-24T04:16:34.999353+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

90 extracted references · 90 canonical work pages · 1 internal anchor

  1. [1]

    A study of the recoverability of computing systems

    Merlin PM. A study of the recoverability of computing systems. Ph.D. thesis, University of California, Irvine, CA, USA, 1974. doi:10.5555/907383

    work page doi:10.5555/907383 1974

  2. [2]

    State Space Abstractions for Time Petri Nets

    Vernadat F, Berthomieu B. State Space Abstractions for Time Petri Nets. In: Son SH, Lee I, Leung JY (eds.), Handbook of Real-Time and Embedded Systems. Chapman and Hall/CRC, 2007. doi:10.1201/ 9781420011746.pt6

    work page 2007

  3. [3]

    Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph

    Traonouez L, Lime D, Roux OH. Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph. In: Formal Modeling and Analysis of Timed Systems (FORMATS 2008), volume 5215 of LNCS. Springer, 2008 pp. 280–294. doi:10.1007/978-3-540-85778-5_20

    work page doi:10.1007/978-3-540-85778-5_20 2008

  4. [4]

    Diagnosis Using Unfoldings of Parametric Time Petri Nets

    Grabiec B, Traonouez L, Jard C, Lime D, Roux OH. Diagnosis Using Unfoldings of Parametric Time Petri Nets. In: Formal Modeling and Analysis of Timed Systems (FORMATS 2010), volume 6246 of LNCS. Springer, 2010 pp. 137–151. doi:10.1007/978-3-642-15297-9_12

    work page doi:10.1007/978-3-642-15297-9_12 2010

  5. [5]

    Precise robustness analysis of time P etri nets with inhibitor arcs

    André E, Pellegrino G, Petrucci L. Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs. In: Formal Modeling and Analysis of Timed Systems (FORMATS’13), volume 8053 of LNCS. Springer, 2013 pp. 1–15. doi:10.1007/978-3-642-40229-6_1

    work page doi:10.1007/978-3-642-40229-6_1 2013

  6. [6]

    Cost Problems for Parametric Time Petri Nets

    Lime D, Roux OH, Seidner C. Cost Problems for Parametric Time Petri Nets. Fundam. Informaticae,

    work page

  7. [7]

    doi:10.3233/FI-2021-2083

    183(1-2):97–123. doi:10.3233/FI-2021-2083

    work page doi:10.3233/fi-2021-2083 2021

  8. [8]

    UPPAAL in a Nutshell

    Lime D, Roux OH, Seidner C, Traonouez L. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), volume 5505 of LNCS. Springer, 2009 pp. 54–57. doi:10.1007/978-3-642-00768-2_6

    work page doi:10.1007/978-3-642-00768-2_6 2009

  9. [9]

    Analyzing resilience properties in oscillatory biological systems using parametric model checking

    Andreychenko A, Magnin M, Inoue K. Analyzing resilience properties in oscillatory biological systems using parametric model checking. Biosystems, 2016. 149:50–58. doi:https://doi.org/10.1016/j.biosystems. 2016.09.002. J. Arias et al. / Formal Analysis and Parameter Synthesis for Time Petri Nets 307

    work page doi:10.1016/j.biosystems 2016

  10. [10]

    Applying Parametric Model- Checking Techniques for Reusing Real-Time Critical Systems

    Parquier B, Rioux L, Henia R, Soulat R, Roux OH, Lime D, André É. Applying Parametric Model- Checking Techniques for Reusing Real-Time Critical Systems. In: Formal Techniques for Safety-Critical Systems (FTSCS 2016), volume 694 of Communications in Computer and Information Science. Springer, 2017 pp. 129–144. doi:https://doi.org/10.1007/978-3-319-53946-1_8

    work page doi:10.1007/978-3-319-53946-1_8 2016

  11. [11]

    Integrated Model-Checking for the Design of Safe and Efficient Distributed Software Commissioning

    Coullon H, Jard C, Lime D. Integrated Model-Checking for the Design of Safe and Efficient Distributed Software Commissioning. In: Integrated Formal Methods (IFM 2019), volume 11918 of LNCS. Springer, Cham, 2019 pp. 120–137. doi:https://doi.org/10.1007/978-3-030-34968-4_7

    work page doi:10.1007/978-3-030-34968-4_7 2019

  12. [12]

    Conditional Rewriting Logic as a Unified Model of Concurrency

    Meseguer J. Conditional Rewriting Logic as a Unified Model of Concurrency. Theor. Comput. Sci., 1992. 96(1):73–155. doi:10.1016/0304-3975(92)90182-F

    work page doi:10.1016/0304-3975(92)90182-f 1992

  13. [13]

    Twenty years of rewriting logic

    Meseguer J. Twenty years of rewriting logic. J. Log. Algebraic Methods Program., 2012. 81(7-8):721–

    work page 2012

  14. [14]

    doi:10.1016/j.jlap.2012.06.003

    work page doi:10.1016/j.jlap.2012.06.003 2012

  15. [15]

    (Springer Berlin Heidelberg, 2009)

    Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott CL. All About Maude – A High-Performance Logical Framework, volume 4350 of LNCS. Springer, 2007. doi:10.1007/978-3-540- 71999-1

    work page doi:10.1007/978-3-540- 2007

  16. [16]

    The Real-Time Maude Tool

    Ölveczky PC, Meseguer J. The Real-Time Maude Tool. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), volume 4963 of LNCS. Springer, 2008 pp. 332–336. doi:10. 1007/978-3-540-78800-3_23

    work page 2008

  17. [17]

    Real-Time Maude and Its Applications

    Ölveczky PC. Real-Time Maude and Its Applications. In: Rewriting Logic and Its Applications (WRLA 2014), volume 8663 of LNCS. Springer, 2014 pp. 42–79. doi:10.1007/978-3-319-12904-4_3

    work page doi:10.1007/978-3-319-12904-4_3 2014

  18. [18]

    Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude

    Ölveczky PC, Meseguer J, Talcott CL. Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. Formal Methods Syst. Des. , 2006. 29(3):253–293. doi:10.1007/ s10703-006-0015-0

    work page 2006

  19. [19]

    Formal Modeling and Analysis of an IETF Multicast Protocol

    Lien E, Ölveczky PC. Formal Modeling and Analysis of an IETF Multicast Protocol. In: Seventh IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009). IEEE Computer Society, 2009 pp. 273–282. doi:10.1109/SEFM.2009.11

    work page doi:10.1109/sefm.2009.11 2009

  20. [20]

    Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude

    Ölveczky PC, Thorvaldsen S. Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theor. Comput. Sci., 2009. 410(2-3):254–280. doi: 10.1016/j.tcs.2008.09.022

    work page doi:10.1016/j.tcs.2008.09.022 2009

  21. [21]

    Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real- Time Maude

    Ölveczky PC, Caccamo M. Formal Simulation and Analysis of the CASH Scheduling Algorithm in Real- Time Maude. In: Fundamental Approaches to Software Engineering (FASE 2006), volume 3922 ofLNCS. Springer, 2006 pp. 357–372. doi:10.1007/11693017_26

    work page doi:10.1007/11693017_26 2006

  22. [22]

    Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study

    Bae K, Krisiloff J, Meseguer J, Ölveczky PC. Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study. Sci. Comput. Program. , 2015. 103:13–50. doi:10.1016/j.scico.2014.09.011

    work page doi:10.1016/j.scico.2014.09.011 2015

  23. [23]

    Formal Modeling and Analysis of Google’s Megastore in Real-Time Maude

    Grov J, Ölveczky PC. Formal Modeling and Analysis of Google’s Megastore in Real-Time Maude. In: Specification, Algebra, and Software – Essays Dedicated to Kokichi Futatsugi, volume 8373 of LNCS. Springer, 2014 pp. 494–519. doi:10.1007/978-3-642-54624-2_25

    work page doi:10.1007/978-3-642-54624-2_25 2014

  24. [24]

    Increasing Consistency in Multi-site Data Stores: Megastore-CGC and Its Formal Analysis

    Grov J, Ölveczky PC. Increasing Consistency in Multi-site Data Stores: Megastore-CGC and Its Formal Analysis. In: Software Engineering and Formal Methods (SEFM 2014), volume 8702 of LNCS. Springer, 2014 pp. 159–174. doi:10.1007/978-3-319-10431-7_12

    work page doi:10.1007/978-3-319-10431-7_12 2014

  25. [26]

    Formal modeling and analysis of safety-critical human multitasking

    Broccia G, Milazzo P, Ölveczky PC. Formal modeling and analysis of safety-critical human multitasking. Innov. Syst. Softw. Eng., 2019. 15(3-4):169–190. doi:10.1007/s11334-019-00333-7

    work page doi:10.1007/s11334-019-00333-7 2019

  26. [27]

    Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude

    Ölveczky PC, Boronat A, Meseguer J. Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. In: Formal Techniques for Distributed Systems, Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010 and 30th IFIP WG 6.1 FORTE 2010, volume 6117 of LNCS. Springer, 2010 pp. 47–62. doi:10.1007/978-3-642-13464-7_5

    work page doi:10.1007/978-3-642-13464-7_5 2010

  27. [28]

    Formal Specification and Analysis of Timing Properties in Software Systems

    AlTurki M, Dhurjati D, Yu D, Chander A, Inamura H. Formal Specification and Analysis of Timing Properties in Software Systems. In: Fundamental Approaches to Software Engineering (FASE 2009), volume 5503 of LNCS. Springer, 2009 pp. 262–277. doi:10.1007/978-3-642-00593-0_18

    work page doi:10.1007/978-3-642-00593-0_18 2009

  28. [30]

    The SynchAADL2Maude Tool

    Bae K, Ölveczky PC, Meseguer J, Al-Nayeem A. The SynchAADL2Maude Tool. In: Fundamental Approaches to Software Engineering (FASE 2012), volume 7212 of LNCS. Springer, 2012 pp. 59–62. doi:10.1007/978-3-642-28872-2_4

    work page doi:10.1007/978-3-642-28872-2_4 2012

  29. [31]

    Semantics, Simulation, and Formal Analysis of Modeling Languages for Embedded Sys- tems in Real-Time Maude

    Ölveczky PC. Semantics, Simulation, and Formal Analysis of Modeling Languages for Embedded Sys- tems in Real-Time Maude. In: Formal Modeling: Actors, Open Systems, Biological Systems – Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, volume 7000 of LNCS, pp. 368–402. Springer, 2011. doi:10.1007/978-3-642-24933-4_19

    work page doi:10.1007/978-3-642-24933-4_19 2011

  30. [32]

    Abstraction and Completeness for Real-Time Maude

    Ölveczky PC, Meseguer J. Abstraction and Completeness for Real-Time Maude. In: 6th International Workshop on Rewriting Logic and its Applications (WRLA 2006), volume 174 of Electronic Notes in Theoretical Computer Science. Elsevier, 2006 pp. 5–27. doi:10.1016/j.entcs.2007.06.005

    work page doi:10.1016/j.entcs.2007.06.005 2006

  31. [33]

    Maude-SE: a Tight Integration of Maude and SMT Solvers

    Yu G, Bae K. Maude-SE: a Tight Integration of Maude and SMT Solvers. In: Preliminary proceedings of WRLA@ETAPS. 2020 pp. 220–232. https://wrla2020.webs.upv.es/pre-proceedings.pdf

    work page 2020

  32. [34]

    Semantics and pragmatics of Real-Time Maude

    Ölveczky PC, Meseguer J. Semantics and pragmatics of Real-Time Maude. High. Order Symb. Comput.,

    work page

  33. [35]

    doi:10.1007/s10990-007-9001-5

    20(1-2):161–196. doi:10.1007/s10990-007-9001-5

    work page doi:10.1007/s10990-007-9001-5

  34. [36]

    Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata

    Arias J, Bae K, Olarte C, Ölveczky PC, Petrucci L, Rømming F. Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata. In: 8th ACM SIGPLAN International Work- shop on Formal Techniques for Safety-Critical Systems (FTSCS 2022). ACM, 2022 pp. 3–15. doi: 10.1145/3563822.3569923

    work page doi:10.1145/3563822.3569923 2022

  35. [37]

    Symbolic Analysis and Parameter Syn- thesis for Networks of Parametric Timed Automata with Global Variables using Maude and SMT Solving

    Arias J, Bae K, Olarte C, Ölveczky PC, Petrucci L, Rømming F. Symbolic Analysis and Parameter Syn- thesis for Networks of Parametric Timed Automata with Global Variables using Maude and SMT Solving. Science of Computer Programming, 2024. 233. doi:10.1016/j.scico.2023.103074

    work page doi:10.1016/j.scico.2023.103074 2024

  36. [38]

    Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving

    Arias J, Bae K, Olarte C, Ölveczky PC, Petrucci L, Rømming F. Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving. In: Application and Theory of Petri Nets and Concurrency (PETRI NETS 2023), volume 13929 of LNCS. Springer, 2023 pp. 369–392. doi: 10.1007/978-3-031-33620-1_20

    work page doi:10.1007/978-3-031-33620-1_20 2023

  37. [39]

    PITPN2Maude, 2024

    Arias J, Bae K, Olarte C, Ölveczky PC, Petrucci L. PITPN2Maude, 2024. URL https://depot.lipn. univ-paris13.fr/real-time-maude/pitpn2maude-journal

    work page 2024

  38. [40]

    Model Checking

    Clarke EM, Grumberg O, Peled DA. Model Checking. MIT Press, 2001. ISBN: 9780262032704

    work page 2001

  39. [41]

    Rewriting modulo SMT and open system analysis

    Rocha C, Meseguer J, Muñoz CA. Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program., 2017. 86(1):269–297. doi:10.1016/j.jlamp.2016.10.001. J. Arias et al. / Formal Analysis and Parameter Synthesis for Time Petri Nets 309

    work page doi:10.1016/j.jlamp.2016.10.001 2017

  40. [42]

    A State Class Based Controller Synthesis Approach for Time Petri Nets

    Leclercq L, Lime D, Roux OH. A State Class Based Controller Synthesis Approach for Time Petri Nets. In: Application and Theory of Petri Nets and Concurrency (PETRI NETS 2023), volume 13929 of LNCS. Springer, 2023 pp. 393–414. doi:10.1007/978-3-031-33620-1_21

    work page doi:10.1007/978-3-031-33620-1_21 2023

  41. [43]

    Symbolic state space reduction with guarded terms for rewriting modulo SMT

    Bae K, Rocha C. Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program., 2019. 178:20–42. doi:10.1016/j.scico.2019.03.006

    work page doi:10.1016/j.scico.2019.03.006 2019

  42. [44]

    Rewriting Logic as a Unifying Framework for Petri Nets

    Stehr M, Meseguer J, Ölveczky PC. Rewriting Logic as a Unifying Framework for Petri Nets. In: Unifying Petri Nets, Advances in Petri Nets, volume 2128 of Lecture Notes in Computer Science . Springer, 2001 pp. 250–303. doi:10.1007/3-540-45541-8_9

    work page doi:10.1007/3-540-45541-8_9 2001

  43. [45]

    Time Petri Nets

    Wang J. Time Petri Nets. In: Timed Petri Nets: Theory and Application, pp. 63–123. Springer, 1998. doi:10.1007/978-1-4615-5537-7_4

    work page doi:10.1007/978-1-4615-5537-7_4 1998

  44. [46]

    Generalized rewrite theories, coherence completion, and symbolic methods

    Meseguer J. Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program., 2020. 110. doi:10.1016/j.jlamp.2019.100483

    work page doi:10.1016/j.jlamp.2019.100483 2020

  45. [47]

    Abstract Logical Model Checking of Infinite-State Systems Using Nar- rowing

    Bae K, Escobar S, Meseguer J. Abstract Logical Model Checking of Infinite-State Systems Using Nar- rowing. In: Rewriting Techniques and Applications (RTA 2013), volume 21 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013 pp. 81–96. doi:10.4230/LIPIcs.RTA.2013.81

    work page doi:10.4230/lipics.rta.2013.81 2013

  46. [48]

    Linear Programming 1: Introduction

    Dantzig G, Thapa M. Linear Programming 1: Introduction. Springer Series in Operations Research and Financial Engineering. Springer New York, 2006. ISBN 9780387226330

    work page 2006

  47. [49]

    Parametric Model-Checking of Stopwatch Petri Nets

    Traonouez L, Lime D, Roux OH. Parametric Model-Checking of Stopwatch Petri Nets. J. Univers. Comput. Sci., 2009. 15(17):3273–3304. doi:10.3217/jucs-015-17-3273

    work page doi:10.3217/jucs-015-17-3273 2009

  48. [50]

    Maude Manual (Version 3.3.1)

    Clavel M, Durán F, Eker S, Escobar S, Lincoln P, Martí-Oliet N, Meseguer J, Rubio R, Talcott C. Maude Manual (Version 3.3.1). SRI International, 2023. Available at http://maude.cs.illinois.edu

    work page 2023

  49. [51]

    Time Petri Nets with Inhibitor Hyperarcs

    Roux OH, Lime D. Time Petri Nets with Inhibitor Hyperarcs. Formal Semantics and State Space Computation. In: Cortadella J, Reisig W (eds.), Applications and Theory of Petri Nets 2004, 25th International Conference, ICATPN 2004, volume 3099 of LNCS. Springer, 2004 pp. 371–390. doi: 10.1007/978-3-540-27793-4_21

    work page doi:10.1007/978-3-540-27793-4_21 2004

  50. [52]

    Petri Nets Are Monoids

    Meseguer J, Montanari U. Petri Nets Are Monoids. Information and Computation, 1990. 88(2):105–155. doi:10.1016/0890-5401(90)90013-8

    work page doi:10.1016/0890-5401(90)90013-8 1990

  51. [53]

    Specification of real-time and hybrid systems in rewriting logic.Theor

    Ölveczky PC, Meseguer J. Specification of real-time and hybrid systems in rewriting logic.Theor. Comput. Sci., 2002. 285(2):359–405. doi:10.1016/S0304-3975(01)00363-2

    work page doi:10.1016/s0304-3975(01)00363-2 2002

  52. [54]

    Rewriting Logic and Petri Nets: A Natural Model for Reconfigurable Distributed Systems

    Capra L. Rewriting Logic and Petri Nets: A Natural Model for Reconfigurable Distributed Systems. In: Distributed Computing and Intelligent Technology (ICDCIT 2022), volume 13145 of LNCS. Springer, 2022 pp. 140–156. doi:10.1007/978-3-030-94876-4_9

    work page doi:10.1007/978-3-030-94876-4_9 2022

  53. [55]

    Canonization of Reconfigurable PT Nets in Maude

    Capra L. Canonization of Reconfigurable PT Nets in Maude. In: Reachability Problems (RP 2022), volume 13608 of LNCS. Springer, 2022 pp. 160–177. doi:10.1007/978-3-031-19135-0_11

    work page doi:10.1007/978-3-031-19135-0_11 2022

  54. [56]

    Model Checking Reconfigurable Petri Nets with Maude

    Padberg J, Schulz A. Model Checking Reconfigurable Petri Nets with Maude. In: 9th International Conference on Graph Transformation (ICGT 2016), volume 9761 of LNCS. Springer, 2016 pp. 54–70. doi:10.1007/978-3-319-40530-8_4

    work page doi:10.1007/978-3-319-40530-8_4 2016

  55. [57]

    SysVeritas: A Framework for Verifying IOPT Nets and Execution Semantics within Embedded Systems Design

    Barbosa PES, Barros JP, Ramalho F, Gomes L, Figueiredo J, Moutinho F, Costa A, Aranha A. SysVeritas: A Framework for Verifying IOPT Nets and Execution Semantics within Embedded Systems Design. In: Technological Innovation for Sustainability - Second IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS 2011), vol...

    work page doi:10.1007/978-3-642-19170-1_28 2011

  56. [58]

    Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints

    Escobar S, López-Rueda R, Sapiña J. Symbolic Analysis by Using Folding Narrowing with Irreducibility and SMT Constraints. In: 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety- Critical Systems (FTSCS 2023). ACM, 2023 pp. 14–25. doi:10.1145/3623503.3623537

    work page doi:10.1145/3623503.3623537 2023

  57. [59]

    Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT

    Lee J, Kim S, Bae K. Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT. In: 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022). ACM, 2022 pp. 56–67. doi:10.1145/3563822.3568016

    work page doi:10.1145/3563822.3568016 2022

  58. [60]

    An extension of HybridSynchAADL and its application to collaborating au- tonomous UA Vs

    Lee J, Bae K, Ölveczky PC. An extension of HybridSynchAADL and its application to collaborating au- tonomous UA Vs. In: Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning (ISoLA 2022), volume 13703 of LNCS. Springer, 2022 pp. 47–64. doi:10.1007/978-3-031- 19759-8_4

    work page doi:10.1007/978-3-031- 2022

  59. [61]

    Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL

    Lee J, Bae K, Ölveczky PC, Kim S, Kang M. Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. International Journal on Software Tools for Technology Transfer, 2022. 24(6):911–948. doi:10.1007/S10009-022-00665-Z

    work page doi:10.1007/s10009-022-00665-z 2022

  60. [62]

    HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL

    Lee J, Kim S, Bae K, Ölveczky PC. HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL. In: Computer Aided Verification (CA V 2021), volume 12759 of LNCS. Springer, 2021 pp. 491–504. doi:10.1007/978-3-030-81685-8_23

    work page doi:10.1007/978-3-030-81685-8_23 2021

  61. [63]

    Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT

    Nigam V , Talcott CL. Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT. In: Rewriting Logic and Its Applications (WRLA 2022), volume 13252 of LNCS. Springer, 2022 pp. 212–229. doi:10.1007/978-3-031-12441-9_11

    work page doi:10.1007/978-3-031-12441-9_11 2022

  62. [64]

    Guarded terms for rewriting modulo SMT

    Bae K, Rocha C. Guarded terms for rewriting modulo SMT. In: International Conference on Formal Aspects of Component Software (FACS 2017). Springer, 2017 pp. 78–97. doi:10.1007/978-3-319-68034- 7_5

    work page doi:10.1007/978-3-319-68034- 2017

  63. [65]

    Coloured Petri Nets, Modelling and Validation of Concurrent Systems

    Jensen K, Kristensen LM. Coloured Petri Nets – Modelling and Validation of Concurrent Systems. Springer, 2009. doi:10.1007/b95112

    work page doi:10.1007/b95112 2009

  64. [66]

    Dickerson

    Arias J, Bae K, Olarte C, Ölveczky PC, Petrucci L, Rømming F. Symbolic Analysis and Parameter Syn- thesis for Time Petri Nets Using Maude and SMT Solving, 2023. doi:10.48550/ARXIV .2303.08929

    work page internal anchor Pith review doi:10.48550/arxiv 2023

  65. [67]

    A Theory of Timed Automata

    Alur R, Dill DL. A Theory of Timed Automata. Theor. Comput. Sci. , 1994. 126(2):183–235. doi: 10.1016/0304-3975(94)90010-8

    work page doi:10.1016/0304-3975(94)90010-8 1994

  66. [68]

    Uppaal SMC tutorial

    David A, Larsen KG, Legay A, Mikucionis M, Poulsen DB. Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf., 2015. 17(4):397–415. doi:10.1007/s10009-014-0361-y

    work page doi:10.1007/s10009-014-0361-y 2015

  67. [69]

    Safe and Optimal Adaptive Cruise Control

    Larsen KG, Mikucionis M, Taankvist JH. Safe and Optimal Adaptive Cruise Control. In: Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, volume 9360 of LNCS. Springer, 2015 pp. 260–277. doi:10.1007/978-3-319-23506-6_17

    work page doi:10.1007/978-3-319-23506-6_17 2015

  68. [70]

    Formal design and analysis of a gear controller.Int

    Lindahl M, Pettersson P, Yi W. Formal design and analysis of a gear controller.Int. J. Softw. Tools Technol. Transf., 2001. 3(3):353–368. doi:10.1007/s100090100048

    work page doi:10.1007/s100090100048 2001

  69. [71]

    On-the-Fly Repairing of Atomicity Violations in ARINC 653 Software

    Choi Et, Kim Th, Jun YK, Lee S, Han M. On-the-Fly Repairing of Atomicity Violations in ARINC 653 Software. Applied Sciences, 2022. 12(4). doi:10.3390/app12042014

    work page doi:10.3390/app12042014 2022

  70. [72]

    Formal Modeling and Verification of the Safety Critical Fire-Fighting Control System

    Wang Y , Wang R, Guan Y , Li X, Wei H, Zhang J. Formal Modeling and Verification of the Safety Critical Fire-Fighting Control System. In: 39th Annual Computer Software and Applications Conference, COMP- SAC Workshops 2015. IEEE Computer Society, 2015 pp. 536–541. doi:10.1109/COMPSAC.2015.181. J. Arias et al. / Formal Analysis and Parameter Synthesis for T...

    work page doi:10.1109/compsac.2015.181 2015

  71. [73]

    Liveness in L/U-Parametric Timed Automata

    Alur R, Henzinger TA, Vardi MY . Parametric real-time reasoning. In: Kosaraju SR, Johnson DS, Aggarwal A (eds.), Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA. ACM, 1993 pp. 592–601. doi:10.1145/167088.167242

    work page doi:10.1145/167088.167242 1993

  72. [74]

    IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability

    André É. IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability. In: Computer Aided Verification (CA V 2021), volume 12759 of LNCS. Springer, 2021 pp. 552–565. doi:10.1007/ 978-3-030-81685-8_26

    work page 2021

  73. [75]

    Vaandrager

    Hune T, Romijn J, Stoelinga M, Vaandrager FW. Linear parametric model checking of timed automata. J. Log. Algebraic Methods Program., 2002. 52-53:183–220. doi:10.1016/S1567-8326(02)00037-1

    work page doi:10.1016/s1567-8326(02)00037-1 2002

  74. [76]

    Bounded Model Checking for Parametric Timed Automata

    Knapik M, Penczek W. Bounded Model Checking for Parametric Timed Automata. Trans. Petri Nets Other Model. Concurr., 2012. 5:141–159. doi:10.1007/978-3-642-29072-5_6

    work page doi:10.1007/978-3-642-29072-5_6 2012

  75. [77]

    Integer Parameter Synthesis for Real-Time Systems

    Jovanovic A, Lime D, Roux OH. Integer Parameter Synthesis for Real-Time Systems. IEEE Trans. Software Eng., 2015. 41(5):445–461. doi:10.1109/TSE.2014.2357445

    work page doi:10.1109/tse.2014.2357445 2015

  76. [78]

    Timed verification of the generic architecture of a memory circuit using parametric timed automata

    Chevallier R, Encrenaz-Tiphène E, Fribourg L, Xu W. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods Syst. Des. , 2009. 34(1):59–81. doi:10.1007/s10703-008-0061-x

    work page doi:10.1007/s10703-008-0061-x 2009

  77. [79]

    The Linear Time- Branching Time Spectrum (Extended Ab- stract)

    Fribourg L, Soulat R, Lesens D, Moro P. Robustness Analysis for Scheduling Problems Using the Inverse Method. In: 19th International Symposium on Temporal Representation and Reasoning (TIME 2012). IEEE Computer Society, 2012 pp. 73–80. doi:10.1109/TIME.2012.10

    work page doi:10.1109/time.2012.10 2012

  78. [80]

    Modeling and analyzing mobile ad hoc networks in Real-Time Maude

    Liu S, Ölveczky PC, Meseguer J. Modeling and analyzing mobile ad hoc networks in Real-Time Maude. J. Log. Algebraic Methods Program., 2016. 85(1):34–66. doi:10.1016/j.jlamp.2015.05.002

    work page doi:10.1016/j.jlamp.2015.05.002 2016

  79. [81]

    Survivability: Design, Formal Mod- eling, and Validation of Cloud Storage Systems Using Maude

    Bobba R, Grov J, Gupta I, Liu S, Meseguer J, Ölveczky PC, Skeirik S. Survivability: Design, Formal Mod- eling, and Validation of Cloud Storage Systems Using Maude. In: Assured Cloud Computing, chapter 2, pp. 10–48. John Wiley & Sons, 2018. https://doi.org/10.1002/9781119428497.ch2

    work page doi:10.1002/9781119428497.ch2 2018

  80. [82]

    A Benchmarks Library for Extended Parametric Timed Au- tomata

    André É, Marinho D, van de Pol J. A Benchmarks Library for Extended Parametric Timed Au- tomata. In: Tests and Proofs (TAP 2021), volume 12740 of LNCS. Springer, 2021 pp. 39–50. doi: 10.1007/978-3-030-79379-1_3

    work page doi:10.1007/978-3-030-79379-1_3 2021

Showing first 80 references.