A First-Order Policy Language for History-Based Transaction Monitoring

DOI10.1007/978-3-642-03466-4_6zbMATH Open1250.68182arXiv0903.2904OpenAlexW1482613269MaRDI QIDQ3393401FDOQ3393401

Authors: Andreas Bauer, Rajeev Goré, Alwen Tiu 

Publication date: 20 August 2009

Published in: Theoretical Aspects of Computing - ICTAC 2009 (Search for Journal in Brave)

Abstract: Online trading invariably involves dealings between strangers, so it is important for one party to be able to judge objectively the trustworthiness of the other. In such a setting, the decision to trust a user may sensibly be based on that user's past behaviour. We introduce a specification language based on linear temporal logic for expressing a policy for categorising the behaviour patterns of a user depending on its transaction history. We also present an algorithm for checking whether the transaction history obeys the stated policy. To be useful in a real setting, such a language should allow one to express realistic policies which may involve parameter quantification and quantitative or statistical patterns. We introduce several extensions of linear temporal logic to cater for such needs: a restricted form of universal and existential quantification; arbitrary computable functions and relations in the term language; and a "counting" quantifier for counting how many times a formula holds in the past. We then show that model checking a transaction history against a policy, which we call the history-based transaction monitoring problem, is PSPACE-complete in the size of the policy formula and the length of the history. The problem becomes decidable in polynomial time when the policies are fixed. We also consider the problem of transaction monitoring in the case where not all the parameters of actions are observable. We formulate two such "partial observability" monitoring problems, and show their decidability under certain restrictions.

Full work available at URL: https://arxiv.org/abs/0903.2904

Recommendations

• Refinement of history-based policies
• Matching Trace Patterns with Regular Policies
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Verification of relational transducers for electronic commerce
• Analysis of dynamic policies

Mathematics Subject Classification ID

Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cited In (8)

• Matching Trace Patterns with Regular Policies
• Monitoring of temporal first-order properties with aggregations
• Trace-length independent runtime monitoring of quantitative policies in LTL
• Foundations of Boolean stream runtime verification
• The ins and outs of first-order runtime verification
• Refinement of history-based policies
• Monitoring metric first-order temporal properties
• Scalable offline monitoring of temporal specifications

This page was built for publication: A First-Order Policy Language for History-Based Transaction Monitoring

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3393401)