English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We continue the investigation of parameterized extensions of Linear TemporalLogic (LTL) that retain the attractive algorithmic properties of LTL: apolynomial space model checking algorithm and a doubly-exponential timealgorithm for solving games. Alur et al. and Kupferman et al. showed that thisis the case for Parametric LTL (PLTL) and PROMPT-LTL respectively, which havetemporal operators equipped with variables that bound their scope in time.Later, this was also shown to be true for Parametric LDL (PLDL), which extendsPLTL to be able to express all omega-regular properties.  Here, we generalize PLTL to systems with costs, i.e., we do not bound thescope of operators in time, but bound the scope in terms of the costaccumulated during time. Again, we show that model checking and solving gamesfor specifications in PLTL with costs is not harder than the correspondingproblems for LTL. Finally, we discuss PLDL with costs and extensions tomultiple cost functions.

Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL