Logic Mining from Process Logs: Towards Automated Specification and Verification

Julia Witek; Radoslaw Klimek

REVIEW 4 major objections 4 minor 43 references

Logic Mining from Process Logs: Towards Automated Specification and Verification

T0 review · 4 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that formal logical specifications can be generated automatically from raw event logs, via process-tree mining and pattern-based translation, and that theorem provers can validate the results for satisfiability…

desk verdict Incremental extension with real-log evaluation, but the PLTL-to-FOL bridge is undefined and the pattern definitions are inconsistent, so the central validation claim fails. read the letter →

arxiv 2506.08628 v1 pith:TAVC5MVT submitted 2025-06-10 cs.SE

Radoslaw Klimek , Julia Witek This is my paper

classification cs.SE MSC 68Q6068T27

keywords processminingeventlogsworkflowtreeslogicalspecificationgenerationpropositionallineartemporallogicautomatedtheoremprovingnoiseanalysis

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper tries to establish that formal specifications for business processes can be extracted automatically from raw event logs and then checked by automated theorem provers, with nobody hand-writing the logic. The route is: mine the log into a process tree with the Inductive Miner, rewrite the tree into one of a fixed set of behavioural patterns (sequence, choice, concurrency, loop), translate each pattern into propositional linear temporal logic, and feed the composed specification to first-order provers. The experiments cover four event logs, including real hospital-billing and loan-application data, at several noise thresholds, checking satisfiability, logical entailment between specifications, and compliance with hand-written safety and liveness requirements. If the claim holds, the practical consequence is that event data alone can produce testable formal models, removing a major manual bottleneck in formal verification.

What carries the argument

The carrying mechanism is a fixed, reusable library of ten pattern templates — sequential composition (Seq2 through Seq5), exclusive choice (Xor2, Xor3), parallel composition (And2 through And4), and Loop — each with a canned propositional linear temporal logic formula. Sequence patterns, for example, contribute an eventual-appearance clause, response chains of the form $\square(a \Rightarrow \Diamond b)$, and mutual-exclusion clauses $\square\neg(a \wedge b)$; choice, parallelism, and loop patterns contribute analogous templates. An event log is first converted by the Inductive Miner into a process tree, the tree is read off as a pattern expression $W$, and the templates are composed into a single specification $L$. That specification is translated to first-order logic by replacing $\square$ and $\Diamond$ with universal and existential quantifiers and given to the E and Vampire theorem provers in TPTP form, whose SZS statuses are the experimental evidence.

What would settle it

Re-run the requirement checks (Problems 11–16, 21–22, 27–28) with a PLTL-native model checker on the same process trees and compare verdicts with the SZS statuses reported by E and Vampire; any mismatch — for example a liveness formula the FOL provers mark Theorem but the temporal tool refutes on a concrete trace — would show the quantified translation changes meaning, so the reported results certify the encoding rather than the intended temporal specification.

Watch

Extended reading notes

Core claim

On its own terms, the paper's central discovery is that the whole chain from event log to verified logical specification runs end to end on every tested log, and that the prover results match the structure of the mined models. Well-behaved logs produce satisfiable specifications; when the noise threshold of the Inductive Miner is raised, the mined tree changes and a liveness requirement that was provable before becomes falsified (Problem 15), while a safety requirement stays provable — so noise degrades the guarantees in a structured, interpretable way. The real-world logs behave similarly: the hospital log at noise 0 is satisfiable and its liveness requirements are provable, but its noise-0.25 specification is unsatisfiable, while the loan-application log is unsatisfiable at noise 0 and satisfiable at 0.25. The paper presents these outcomes as evidence that the pattern library is sufficient for realistic workflows, that the method degrades gracefully, and that the pattern set can be extended when needed, as shown by the newly added And4 pattern.

Load-bearing premise

The whole validation chain stands on the assumption that replacing the temporal operators $\square$ and $\Diamond$ with universal and existential quantifiers preserves the behaviours being tested, an approximation the paper itself acknowledges.

Editorial extensions

If this is right

New event logs can be added to the pipeline without writing new logic: only the mining step is log-specific, because the pattern templates are fixed and reused.
Noise has a structured effect: raising the Inductive Miner's threshold can turn a previously provable liveness requirement into a falsified conjecture while leaving a safety requirement provable, so practitioners can see which guarantees degrade as data quality worsens.
The provers can automatically flag inconsistency: both real-world logs produced specifications judged unsatisfiable at one of the noise levels, so the pipeline can surface problems rather than merely confirming good models.
The fixed pattern set proved sufficient for every log in the study, and the addition of And4 shows the library can grow to fit new process structures without changing the core translation method.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The most direct extension is continuous conformance testing: re-mine a log periodically, regenerate the specification, and let a prover check whether new observations still entail the old safety and liveness requirements.
The reliance on process trees sets a boundary: logs whose control flow is fundamentally unstructured or cyclic would need preprocessing before the pattern set can cover them, which the paper itself flags as a remark rather than a solved problem.
Because silent (null) activities are inserted purely to complete pattern shapes and then appear inside formulas such as the safety requirement $\square\neg(Inform\_user \wedge null)$, users should audit these artificial activities before trusting the verification verdicts.
A quantitative noise study would sharpen the qualitative finding: sweep the noise threshold in small steps and measure the fraction of liveness versus safety requirements that remain provable, testing whether degradation is monotone in noise.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's my take. The paper extends the pattern-based logic generation you already published to process trees mined from event logs, and the new empirical material—two real-world logs, noise-level variations, and the And4 pattern—is the genuine contribution. The pipeline is clearly described, and the threats-to-validity section is honest about some limitations. That is where the credit stops.

The stress-test note lands squarely. Section 4 says you replace □ and ◇ with universal and existential quantifiers, but no first-order signature is given: no ordering relation, no trace domain, no quantifier-scope rules. Replacing □¬(a∧b) with ∀x ¬(A(x)∧B(x)) is only equivalent if the domain is exactly the set of time points, and even then "later" is lost in formulas like □(a ⇒ ◇b). So the SZS statuses in Tables 4–8 say nothing about the PLTL specifications you claim to validate. The paper's own admission that "semantics is only approximated" is candid but fatal for the main conclusion.

There is also a straightforward internal contradiction in Table 1. Seq2(a,b) includes a and b as initial formulas and then □¬(a∧b), which is inconsistent at time zero. The same pattern repeats in Seq3 and friends. That is not a subtle semantic point; it is a basic logical error.

The prover results reflect the confusion. Problem19 is Theorem for Vampire and ContradictoryAxioms for E. Problems 18 and 23 return Unsatisfiable, yet the paper does not treat those as failures—it says "specification unsatisfied" and still concludes the method works. An unsatisfiable generated specification is either a bug in the encoding or a genuine conflict in the pattern composition; either way it undermines the claim that the pipeline produces testable specifications.

Who is this for? Someone scouting pipeline ideas in process mining and formal verification might read it as a sketch. But as a research claim, the validation is not there. I would not send this to peer review in its current form. The authors would need to provide the actual PLTL-to-FOL translation, show it preserves truth, and correct the pattern definitions—or switch to a native PLTL prover—before the empirical results can be taken seriously.

Referee Report

4 major / 4 minor

Summary. The paper proposes an automated pipeline that takes event logs, applies the Inductive Miner to obtain process trees, maps tree fragments onto a fixed set of behavioural patterns (Seq2--Seq5, Xor2--Xor3, And2--And4, Loop), translates each pattern into propositional linear temporal logic (PLTL) formulas, and then validates the resulting specifications with first-order logic (FOL) theorem provers (E and Vampire) via TPTP encoding. The evaluation covers two illustrative logs and two real-world logs (Hospital Billing, BPI Challenge 2012), including variations of the noise threshold. The paper claims that the pattern set is sufficient, that the generated specifications are satisfiable and internally consistent, that they satisfy hand-written liveness and safety requirements, and that the overall pipeline is end-to-end feasible (Facts 1--7).

Significance. If the technical core were sound, the paper would offer a useful bridge between process mining and formal specification: it is a genuine attempt to automate the derivation of testable logical specifications from raw event data, it uses publicly available real-world logs, and the tooling was independently re-implemented. The empirical breadth (four logs, two real-world cases, multiple noise levels) is a strength relative to earlier work. However, the central validation step rests on an unspecified and admittedly approximate PLTL-to-FOL translation, the pattern definitions in Table 1 are internally inconsistent as written, and several reported prover results are mutually contradictory. These issues are load-bearing: they undermine the paper's main claims that the generated specifications are logically validated and that the full pipeline works end to end. The contribution is therefore not currently established.

major comments (4)

[Section 4, PLTL-to-FOL simplification] The translation from PLTL to FOL is neither defined nor shown to be semantics-preserving. The paper states that the □ and ◇ operators are replaced by universal and existential quantifiers, respectively, and Section 6 concedes that 'semantics is only approximated.' No axiomatization of trace ordering, time-point domain, or quantifier scope is provided, and no example TPTP encoding is given. This matters because PLTL formulas are evaluated over infinite traces with a temporal order, whereas FOL formulas range over arbitrary first-order structures. For instance, □(a ⇒ ◇b) requires every a-state to be followed by a later b-state, but a naive ∀x∃y(A(x) ⇒ B(y)) neither enforces y to be later than x nor restricts quantification to time points. Consequently, the SZS statuses in Tables 4--8 do not establish anything about the PLTL specifications the paper claims to generate and validate, and Fact 5 and the RQ2 conclusions are unsupported.
[Table 1, pattern definitions] The logical pattern definitions in Table 1 are internally inconsistent as written. For example, Seq2(a,b) is the conjunction ⟨a, b, ✸a, □(a ⇒ ✸b), □¬(a∧b)⟩; the standalone formula b asserts that b holds at the initial state, while □¬(a∧b) forbids a∧b at every state, including the initial one, so the conjunction is unsatisfiable unless a and b are not both asserted initially. The same issue appears in Seq3 and Seq4, where a and c, or a and d, are both asserted at the initial state while □¬(a∧c) or □¬(a∧d) is also included. Yet Table 4 reports the generated specifications as satisfiable. This means either the intended PLTL reading of the tuple notation is different from what the paper states, or the TPTP encoding does not correspond to Table 1; in either case the satisfiability results do not validate the specifications as defined.
[Tables 7 and 8, contradictory prover results] Several reported prover outputs are mutually contradictory and are not discussed, yet they are used to support Fact 6. In Problem19, Vampire returns SZS status Theorem while E returns ContradictoryAxioms; if the axioms are contradictory, the Theorem status is vacuous. Problems 21 and 22 list SZS status Theorem for both provers but the comment columns read 'Conjecture falsified', which is internally inconsistent with a Theorem status. Furthermore, Problems 18 and 23 are Unsatisfiable, meaning the specifications have no model; the tables label this 'Specification unsatified' but the paper does not acknowledge that these are failed satisfiability tests. The Discussion section (RQ2) claims that the specifications 'were systematically subjected to property-based testing... providing evidence of internal coherence,' which is contradicted by its own data.
[Section 4.5 and Section 6, circularity of validation requirements] The requirements used for validation are not independent of the pattern semantics. Formulas (6)--(9) are hand-written to mirror the very shapes that the pattern translation produces (e.g., Formula (6) is a liveness implication of the same form as the Seq and Xor pattern clauses, and Formula (7) is a mutual-exclusion formula of the same form as the □¬(a∧b) clauses). Verifying that a generated specification implies such a requirement is therefore close to verifying a tautological consequence of the pattern templates, not aligning the mined model with an externally given domain requirement. Section 6 frames the internal-validity threat only in terms of encoding stability; it does not address the construct-validity issue that the requirements are derived from the same pattern set as the specifications. An external benchmark or at least requirements expressed independently of Σ would be needed to support the claim of requirement compliance.

minor comments (4)

[Throughout] The paper contains numerous typographical errors that should be corrected in any revision: 'par ticularly' in the abstract, 'Satifsiable' in Table 6, 'staus' in Table 4, 'Chalenge' in the caption of Figure 10, 'ralationship' in Section 5, and 'unsatified' in Tables 7 and 8.
[Section 4.2] Table 4 and Table 5 captions are ungrammatical ('for the four basic logical specifications obtained' and 'or the logical relationships'), and the font of the SZS outputs makes it hard to distinguish raw prover comments from the authors' interpretations; a cleaner presentation of the results tables would improve readability.
[References] Reference [42] lists only 'Semczyszyn' as the second author without a first name or initials, which is incomplete for a formal publication.
[Section 3.2, Fact 1] Fact 1 asserts that the pattern set is supported by empirical evidence across four event logs, but the set is fixed a priori and And4 was added after observing the logs; the claim should be presented as a post-hoc observation rather than a validated completeness result.

Circularity Check

2 steps flagged · score 6.0 of 10

Partial circularity: several 'requirement validation' checks reduce to testing the very pattern conjuncts that define the generated specification, so part of the empirical validation is forced by construction.

self definitional [Section 4.5, Formulas (6)-(9), Table 6; compared with Table 1 pattern definitions]
"For the speciﬁcation of Problem 1, two requirements have been deﬁned, namely liveness: ✷(Register_request ⇒ ✸(Reject_request ∨ P ay_compensation)) (6) and safety: ✷¬(Reject_request ∧ P ay_compensation) (7)"

The safety requirement (7) is literally the conjunct ✷¬(a ∧ b) of the Xor2(s,a,b,e) pattern in Table 1, instantiated with a=Reject_request and b=Pay_compensation. The generated specification L is built by conjoining instances of the Table 1 patterns, so L ⊢ (7) is a tautology. Likewise Formula (9), ✷¬(Inform_user ∧ null), is a consequence of the And2 conjunct ✷¬(s ∧ (a∨b)) when s is the null activity. Reporting SZS Theorem for Problems 12, 14, and 16 therefore validates the specification against requirements that were copied from the same pattern definition that generates L, not against independent domain constraints.
fitted input called prediction [Section 3.2, Formula (1) and Fact 1]
"Our experiments with the Inductive Miner indicate that the following set of approved patterns is suﬃcient: Π = {Seq2, Seq3, Seq4, Seq5, Xor2, Xor3, And2, And3, And4, Loop} (1)"

The approved pattern set Π is presented as a discovery from the same experiments ('Our experiments ... indicate that ... is sufficient'), and the And4 pattern is said to have 'emerged from the analysis of the two real-world event logs.' Fact 1 then cites these same four logs as empirical support for the sufficiency of Π. The evidence is therefore the training data that determined the pattern set; no independent or held-out benchmark is used to test whether Π is sufficient. This is a self-confirmation of the pattern set rather than an external prediction.

full rationale

The core empirical pipeline—mining public event logs with the Inductive Miner, building process trees, and generating compositional PLTL specifications—is new, uses real data, and does not fit numeric parameters, so the overall approach is not entirely circular. However, the validation category is partially circular: the safety requirements in Formula (7) and Formula (9) coincide with conjuncts already present in the Table 1 pattern definitions, making the implication checks Problems 12, 14, and 16 tautological. Fact 1 also confirms the sufficiency of the pattern set on the very logs that determined it. The PLTL-to-FOL simplification, explicitly acknowledged as approximating semantics, is a validity threat rather than a circular step. The self-citations to [3,28] for satisfiability preservation and relative completeness are prior work by the same authors; they are load-bearing for the generation method's soundness, but they are not the main source of circularity here. Overall, the existence of a working end-to-end pipeline is supported, but some of the reported 'validation' results are forced by construction, yielding a partial circularity score of 6.

Assumptions & free parameters 2 free parameters · 4 assumptions · 1 invented entities

The central claim relies on several unverified assumptions: the representational adequacy of process trees, the faithfulness of the FOL simplification, the sufficiency of the pattern set, and the semantic transparency of inserted tau activities. No independent evidence is provided for these assumptions.

free parameters (2)

Noise threshold = 0, 0.25, 0.5, 1
The Inductive Miner noise threshold is varied in the experiments; the paper does not justify the specific values and does not report the 'default' value used for Problems 1 and 2, making the parameter choice not reproducible.
And4 pattern inclusion = post hoc addition
The pattern And4 was added after observing the real-world logs, adapting the pattern set to the data rather than testing a pre-specified representation.

assumptions (4)

domain assumption Every event log can be adequately represented as a process tree produced by the Inductive Miner.
Remark 1 and Section 3.1; unstructured or cyclic models are assumed to be preprocessable; the experimental logs all produced trees, but no formal conditions are given.
ad hoc to paper The FOL encoding obtained by replacing □ with ∀ and ◇ with ∃ preserves the logical properties of the original PLTL specification.
Section 4 explicitly substitutes PLTL operators with quantifiers; without an explicit time/order relation this is not a sound translation, yet all theorem proving results depend on it.
domain assumption The fixed pattern set Π covers all relevant behaviour in the analyzed logs.
Fact 1 and Fact 7, based only on the four logs used in this study; no proof of completeness is given.
ad hoc to paper Inserting null/silent activities (tau) to complete pattern structures does not alter the behavioural properties under verification.
Section 3.2, Remarks 2 and 3; the paper assumes tau insertions are semantics-preserving but does not check this on the original logs.

invented entities (1)

Null/silent activities (tau)
purpose: Internal nodes to complete pattern shapes when an entry or exit point is missing in the mined tree.
These are artificial placeholders with no counterpart in the event logs; the paper invokes the process-mining convention (Remark 3) but does not show that their insertion preserves the semantics of the original log.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Logic Mining from Process Logs: Towards Automated Specification and Verification." pith.science (2026). https://pith.science/paper/TAVC5MVT

@misc{pith2026250608628,
  author       = {Pith},
  title        = {Pith review of: Logic Mining from Process Logs: Towards Automated Specification and Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TAVC5MVT}},
  note         = {Machine review of arXiv:2506.08628}
}

read the original abstract

Logical specifications play a key role in the formal analysis of behavioural models. Automating the derivation of such specifications is particularly valuable in complex systems, where manual construction is time-consuming and error-prone. This article presents an approach for generating logical specifications from process models discovered via workflow mining, combining pattern-based translation with automated reasoning techniques. In contrast to earlier work, we evaluate the method on both general-purpose and real-case event logs, enabling a broader empirical assessment. The study examines the impact of data quality, particularly noise, on the structure and testability of generated specifications. Using automated theorem provers, we validate a variety of logical properties, including satisfiability, internal consistency, and alignment with predefined requirements. The results support the applicability of the approach in realistic settings and its potential integration into empirical software engineering practices.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

43 extracted references · 35 canonical work pages

[1]

Hi story and Philosophy of Logic 36(3), 195–204 (2015) https://doi.org/10.1080/01445340.2015.1084183 29

Mol, L.D., Primiero, G.: When logic meets engineering: I ntroduction to logical issues in the history and philosophy of computer science. Hi story and Philosophy of Logic 36(3), 195–204 (2015) https://doi.org/10.1080/01445340.2015.1084183 29

work page arXiv 2015
[2]

In: Paule, P

Broy, M.: On the role of logic and algebra in software engi neering. In: Paule, P. (ed.) Mathematics, Computer Science and Logic – A N ever End- ing Story: The Bruno Buchberger Festschrift, pp. 51–68. Spr inger, ??? (2013). https://doi.org/10.1007/978-3-319-00966-7_2

work page doi:10.1007/978-3-319-00966-7_2 2013
[3]

Journal of Logical and Algebraic Methods in Programming 104, 201–226 (2019) https://doi.org/10.1016/j.jlamp.2019.02.005

Klimek, R.: Pattern-based and composition-driven auto matic generation of logical speciﬁcations for workﬂow-oriented software mo dels. Journal of Logical and Algebraic Methods in Programming 104, 201–226 (2019) https://doi.org/10.1016/j.jlamp.2019.02.005

work page doi:10.1016/j.jlamp.2019.02.005 2019
[4]

Springer, ??? (2016)

Aalst, W.M.P.: Process Mining: Data Science in Action, 2 nd edn. Springer, ??? (2016). https://doi.org/10.1007/978-3-662-49851-4

doi:10.1007/978-3-662-49851-4 2016
[5]

IEEE Transactions on Knowledge and Da ta Engineering 31(4), 686–705 (2019) https://doi.org/10.1109/TKDE.2018.2841877

Augusto, A., Conforti, R., Dumas, M., Rosa, M.L., Maggi, F.M., Marrella, A., Mecella, M., Soo, A.: Automated discovery of process models from event logs: Review and benchmark. IEEE Transactions on Knowledge and Da ta Engineering 31(4), 686–705 (2019) https://doi.org/10.1109/TKDE.2018.2841877

work page arXiv 2019
[6]

In: Knowledge Sci- ence, Engineering and Management: 12th International Conf erence, KSEM 2019, Athens, Greece, August 28–30, 2019, Proceedings, Part II 12 , pp

Wiśniewski, P., Kluza, K., Jobczyk, K., Stachura-Terle cka, B., Ligeza, A.: Overview of generation methods for business process models . In: Knowledge Sci- ence, Engineering and Management: 12th International Conf erence, KSEM 2019, Athens, Greece, August 28–30, 2019, Proceedings, Part II 12 , pp. 55–60 (2019). Springer

work page 2019
[7]

IEEE Transactions on Knowledge and Data Engineering 16(9), 1128–1142 (2004) https://doi.org/10.1109/TKDE.2004.47

Aalst, W., Weijters, T., Maruster, L.: Workﬂow mining: d iscovering process mod- els from event logs. IEEE Transactions on Knowledge and Data Engineering 16(9), 1128–1142 (2004) https://doi.org/10.1109/TKDE.2004.47

doi:10.1109/tkde.2004.47 2004
[8]

BETA Working Paper Series, WP 166, Eindhoven Uni versity of Technology, Eindhoven (2006)

Weijters, A., Aalst, W., Medeiros, A.: Process Mining wi th the Heuristics Miner- algorithm. BETA Working Paper Series, WP 166, Eindhoven Uni versity of Technology, Eindhoven (2006)

work page 2006

Show all 43 references

[9]

In: Lohmann, N., Song, M., Wohed, P

Leemans, S.J.J., Fahland, D., Aalst, W.M.P.: Discoveri ng block-structured pro- cess models from event logs containing infrequent behaviou r. In: Lohmann, N., Song, M., Wohed, P. (eds.) Business Process Management Work shops - BPM 2013 International Workshops, Beijing, China, ...

2013 doi
[10]

In: Business Process Man agement Work- shops

Brzychczy, E., Kluza, K., Szała, L.: Enhancement of low- level event abstraction with large language models (llms). In: Business Process Man agement Work- shops. BPM 2024 International Workshops, Krakow, Poland, S eptember 1–6, 2024, Revised Selected Papers, pp. 209–220 (2025)...

2025
[11]

Mendling, J., Lassen, K.B., Zdun, U.: On the transforma tion of con- trol ﬂow between block-oriented and graph-oriented proces s modelling languages. Int. J. Bus. Process. Integr. Manag. 3(2), 96–108 (2008) 30 https://doi.org/10.1504/IJBPIM.2008.020973

2008 arXiv
[12]

: From bpmn process models to bpel web services

Ouyang, C., Dumas, M., Hofstede, A.H.M., Aalst, W.M.P. : From bpmn process models to bpel web services. In: IEEE International Confere nce on Web Services (ICWS’06), pp. 285–292 (2006)

2006
[13]

In: L atour, T., Petit, M

Recker, J.C., Mendling, J.: On the translation between bpmn and bpel: Con- ceptual mismatch between process modeling languages. In: L atour, T., Petit, M. (eds.) 18th International Conference on Advanced Inform ation Systems Engineering, pp. 521–532. Namur University Press, ??...
[14]

Information and Software Technology 50(3), 131–159 (2008) https://doi.org/10.1016/j.infsof.2006.11.004

van der Aalst, W.M.P., Bisgaard Lassen, K.: Translatin g unstructured workﬂow processes to readable bpel: Theory and implementa- tion. Information and Software Technology 50(3), 131–159 (2008) https://doi.org/10.1016/j.infsof.2006.11.004

2008 doi
[15]

Algorithms 13(11) (2020) https://doi.org/10.3390/a13110279

Zelst, S.J., Leemans, S.J.J.: Translating workﬂow net s to process trees: An algo- rithmic approach. Algorithms 13(11) (2020) https://doi.org/10.3390/a13110279

2020 doi
[16]

In: Perner, P

Ferilli, S.: The woman formalism for expressing proces s models. In: Perner, P. (ed.) Advances in Data Mining. Applications and Theoretica l Aspects, pp. 363–
[17]

In: Kłopotek, M.A., Wierzchoń, S.T., Trojanowski, K

Roubtsova, E.E.: Property driven mining in workﬂow log s. In: Kłopotek, M.A., Wierzchoń, S.T., Trojanowski, K. (eds.) Intelligent Infor mation Processing and Web Mining, pp. 471–475. Springer, Berlin, Heidelberg (200 5)
[18]

In: Leeuwen, J

Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J . (ed.) Handbook of Theoretical Computer Science vol. B, pp. 995–1072. MIT Pres s, ??? (1990). http://dl.acm.org/citation.cfm?id=114891.114907

1990
[19]

Springer, ??? (1992)

Manna, Z., Pnueli, A.: The Temporal Logic of Reactive an d Concurrent Systems – Speciﬁcation. Springer, ??? (1992)

1992
[20]

In: Meersm an, R., Tari, Z

Aalst, W.M.P., Beer, H.T., Dongen, B.F.: Process minin g and veriﬁcation of properties: An approach based on temporal logic. In: Meersm an, R., Tari, Z. (eds.) On the Move to Meaningful Internet Systems 2005: Coop IS, DOA, and ODBASE, pp. 130–147. Springer, Berlin, Heidelberg (2005)

2005
[21]

In: Proceedings of the 39th IEEE/AC M Inter- national Conference on Automated Software Engineering Wor kshops (ASE/RENE), Sun 27 October–Fri 1 November 2024, Sacramento , CA, USA

Klimek, R., Witek, J.: Automatic generation of logical speciﬁcations for behavioural models. In: Proceedings of the 39th IEEE/AC M Inter- national Conference on Automated Software Engineering Wor kshops (ASE/RENE), Sun 27 October–Fri 1 November 2024, Sacramento , CA, USA. ASEW...

2024
[22]

In: Zalta, E.N

Szabó, Z.G.: Compositionality. In: Zalta, E.N. (ed.) S tanford Encyclope- dia of Philosophy HTTP://PLATO.STANFORD.EDU/ENTRIES/COMPOSITIONALITY/ (2012). accessed on 20-Feb-2018

2012
[23]

In: Werning, M., Hinzen, W., Machery, E

Recanati, F.: Composition ality, ﬂexibility, and cont ext dependence. In: Werning, M., Hinzen, W., Machery, E. (eds.) The Oxford Handb ook of Compositionality, pp. 175–191. Oxford Handbook Online, ??? (2012). https://doi.org/10.1093/oxfordhb/9780199541072.013.0008

2012
[24]

Proceedings of the IEEE 104(5), 960–972 (2016) https://doi.org/10.1109/JPROC.2015.2510366

Tripakis, S.: Compositionality in the science of syste m design. Proceedings of the IEEE 104(5), 960–972 (2016) https://doi.org/10.1109/JPROC.2015.2510366

2016
[25]

Psicothema 30, 322–329 (2018)

Bogarín, A., Cerezo, R., Romero, C.: Discovering learn ing processes using induc- tive miner: A case study with learning management systems (l mss). Psicothema 30, 322–329 (2018)

2018
[26]

Data & Knowledge Engineering 69(10), 999–1021 (2010) https://doi.org/10.1016/j.datak.2010.06.001

Wen, L., Wang, J., Aalst, W.M.P., Huang, B., Sun, J.: Min ing process models with prime invisible tasks. Data & Knowledge Engineering 69(10), 999–1021 (2010) https://doi.org/10.1016/j.datak.2010.06.001

2010 doi
[27]

Information System s 124, 102383 (2024) https://doi.org/10.1016/J.IS.2024.102383

Leemans, S.J.J., Maggi, F.M., Montali, M.: Enjoy the si lence: Analysis of stochas- tic petri nets with silent transitions. Information System s 124, 102383 (2024) https://doi.org/10.1016/J.IS.2024.102383

2024
[28]

International Journal of Applied Mathema tics and Computer Science 24(4), 941–956 (2014) https://doi.org/10.2478/amcs-2014-0069

Klimek, R.: A system for deduction-based formal veriﬁc ation of workﬂow-oriented software models. International Journal of Applied Mathema tics and Computer Science 24(4), 941–956 (2014) https://doi.org/10.2478/amcs-2014-0069

2014 doi
[29]

Journal of Indian Council of Philosophical Research XXVII(1), 249–276 (2011)

Wolter, F., Wooldridge, M.: Temporal and dynamic logic . Journal of Indian Council of Philosophical Research XXVII(1), 249–276 (2011)

2011
[30]

Bibli otheca Mathematica

Kleene, S.C.: Introduction to Metamathematics. Bibli otheca Mathematica. North-Holland, ??? (1952)

1952
[31]

Handbook of Logic in Artiﬁ cial Intelligence and Logic Programming

Benthem, J.: Temporal Logic. Handbook of Logic in Artiﬁ cial Intelligence and Logic Programming. 4, pp. 241–350. Clarendon Press, ??? (19 93–95)
[32]

accessed on 5-Aug-202 4 (2020)

Schulz, S.: Website for prover E. accessed on 5-Aug-202 4 (2020). http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html

2020
[33]

Journal of AI C ommunications 15(2,3), 111–126 (2002)

Schulz, S.: E – a brainiac theorem prover. Journal of AI C ommunications 15(2,3), 111–126 (2002)

2002
[34]

accessed on 5 -Aug-2024 (2017)

Voronkov, A.: Website for prover Vampire. accessed on 5 -Aug-2024 (2017). https://vprover.github.io/

2017
[35]

Journal of AI Communications 15(2,3), 91–110 (2002) 32

Riazanov, A., Voronkov, A.: The design and implementat ion of V AMPIRE. Journal of AI Communications 15(2,3), 91–110 (2002) 32

2002
[36]

Journal of Automated Reasoning 59, 438–502 (2017)

Sutcliﬀe, G.: The TPTP Problem Library and Associated I nfrastructure. Journal of Automated Reasoning 59, 438–502 (2017)

2017
[37]

The last access 25.04.2024 (2023)

Schreiner, W.: First-order logic: software for provin g, Course ’Computational logic’, https://moodle.risc.jku.at/pluginﬁle.php/11902/mod_resource/content/9/10-fol6.pdf . The last access 25.04.2024 (2023)

2023
[38]

IEEE Transactions on Software Engineering 3(2), 125–143 (1977) https://doi.org/10.1109/TSE.1977.229904

Lamport, L.: Proving the correctness of multiprocess p rograms. IEEE Transactions on Software Engineering 3(2), 125–143 (1977) https://doi.org/10.1109/TSE.1977.229904

1977
[39]

Inform ation Processing Letters 21 (4), 181–185 (1985)

Alpern, B., Schneider, F.B.: Deﬁning liveness. Inform ation Processing Letters 21 (4), 181–185 (1985)

1985
[40]

EATCS-Bulletin 53 (1994)

Kindler, E.: Safety and liveness properties: A survey. EATCS-Bulletin 53 (1994)

1994
[41]

Springer, ??? (2012)

Ben-Ari, M.: Mathematical Logic for Computer Science, 3rd edn. Springer, ??? (2012)

2012
[42]

In: Proceedings of the 29th International Confer ence on Evaluation and Assessment in Software Engineering (EASE 2025), 17–20 June , 2025, Istanbul, Turkey

Klimek, R., Semczyszyn: Re-evaluation of logical spec iﬁcation in behavioural ver- iﬁcation. In: Proceedings of the 29th International Confer ence on Evaluation and Assessment in Software Engineering (EASE 2025), 17–20 June , 2025, Istanbul, Turkey. Search Also Preprints, http...

2025 arXiv
[378]

Springer, Cham (2016)

2016

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

Hi story and Philosophy of Logic 36(3), 195–204 (2015) https://doi.org/10.1080/01445340.2015.1084183 29

Mol, L.D., Primiero, G.: When logic meets engineering: I ntroduction to logical issues in the history and philosophy of computer science. Hi story and Philosophy of Logic 36(3), 195–204 (2015) https://doi.org/10.1080/01445340.2015.1084183 29

work page arXiv 2015

[2] [2]

In: Paule, P

Broy, M.: On the role of logic and algebra in software engi neering. In: Paule, P. (ed.) Mathematics, Computer Science and Logic – A N ever End- ing Story: The Bruno Buchberger Festschrift, pp. 51–68. Spr inger, ??? (2013). https://doi.org/10.1007/978-3-319-00966-7_2

work page doi:10.1007/978-3-319-00966-7_2 2013

[3] [3]

Journal of Logical and Algebraic Methods in Programming 104, 201–226 (2019) https://doi.org/10.1016/j.jlamp.2019.02.005

Klimek, R.: Pattern-based and composition-driven auto matic generation of logical speciﬁcations for workﬂow-oriented software mo dels. Journal of Logical and Algebraic Methods in Programming 104, 201–226 (2019) https://doi.org/10.1016/j.jlamp.2019.02.005

work page doi:10.1016/j.jlamp.2019.02.005 2019

[4] [4]

Springer, ??? (2016)

Aalst, W.M.P.: Process Mining: Data Science in Action, 2 nd edn. Springer, ??? (2016). https://doi.org/10.1007/978-3-662-49851-4

doi:10.1007/978-3-662-49851-4 2016

[5] [5]

IEEE Transactions on Knowledge and Da ta Engineering 31(4), 686–705 (2019) https://doi.org/10.1109/TKDE.2018.2841877

Augusto, A., Conforti, R., Dumas, M., Rosa, M.L., Maggi, F.M., Marrella, A., Mecella, M., Soo, A.: Automated discovery of process models from event logs: Review and benchmark. IEEE Transactions on Knowledge and Da ta Engineering 31(4), 686–705 (2019) https://doi.org/10.1109/TKDE.2018.2841877

work page arXiv 2019

[6] [6]

In: Knowledge Sci- ence, Engineering and Management: 12th International Conf erence, KSEM 2019, Athens, Greece, August 28–30, 2019, Proceedings, Part II 12 , pp

Wiśniewski, P., Kluza, K., Jobczyk, K., Stachura-Terle cka, B., Ligeza, A.: Overview of generation methods for business process models . In: Knowledge Sci- ence, Engineering and Management: 12th International Conf erence, KSEM 2019, Athens, Greece, August 28–30, 2019, Proceedings, Part II 12 , pp. 55–60 (2019). Springer

work page 2019

[7] [7]

IEEE Transactions on Knowledge and Data Engineering 16(9), 1128–1142 (2004) https://doi.org/10.1109/TKDE.2004.47

Aalst, W., Weijters, T., Maruster, L.: Workﬂow mining: d iscovering process mod- els from event logs. IEEE Transactions on Knowledge and Data Engineering 16(9), 1128–1142 (2004) https://doi.org/10.1109/TKDE.2004.47

doi:10.1109/tkde.2004.47 2004

[8] [8]

BETA Working Paper Series, WP 166, Eindhoven Uni versity of Technology, Eindhoven (2006)

Weijters, A., Aalst, W., Medeiros, A.: Process Mining wi th the Heuristics Miner- algorithm. BETA Working Paper Series, WP 166, Eindhoven Uni versity of Technology, Eindhoven (2006)

work page 2006