A first-order policy language for history-based transaction monitoring

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, assuming that the underlying interpreted functions and relations are polynomially computable. 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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 94,070

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Similar books and articles

A decidable timeout-based extension of linear temporal logic.Janardan Misra & Suman Roy - 2014 - Journal of Applied Non-Classical Logics 24 (3):262-291.
Handling database updates in two-dimensional temporal logic.Marcelo Finger - 1992 - Journal of Applied Non-Classical Logics 2 (2):201-224.
Decidable fragments of first-order temporal logics.Ian Hodkinson, Frank Wolter & Michael Zakharyaschev - 2000 - Annals of Pure and Applied Logic 106 (1-3):85-134.
Reasoning about sequences of memory states.Rémi Brochenin, Stéphane Demri & Etienne Lozes - 2010 - Annals of Pure and Applied Logic 161 (3):305-323.

Analytics

Added to PP
2010-12-22

Downloads
59 (#266,043)

6 months
59 (#92,629)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references