طريقة للتعبير عن LTL (متغير) لفرض تدفق من البيانات لتلبية بعض المنطق الزمني الخطي

Question

منطق الوقت الخطي (LTL) يستخدم ل التحقق من النظام.في حالتي، أستثمر بعض الوقت لمعرفة مدى جدوى استخدام LTL هذه المرة لفرض قيد على تدفق البيانات.كفى من العموميات، لنأخذ مثالا بسيطا:

المشغل حتى في التعبير u Until v في LTL تعني حدث u حتى v, ، إنها صيغة عامة عدد لا نهائي من آثار الإشارة يمكن أن تلبي.انظر تعريفه هنا:صفحة 4

يحب:

u,u,u,v,v,v,...
u,u,u,u,u,u,...
u,v,v,v,v,v,...

في حالتي، أرغب في فرض صيغ مثل LTL على نظام يتلقى دفقًا من البيانات؛مرة أخرى لنأخذ نفس عامل التشغيل until.

لنفترض أن لدينا إشارتي دخل، واحدة للثابت u، والأخرى للثابت v.

u,u,u,u,u,u,...
 , , , ,v,v,...

معالج الدفق الذي يأخذ هذه المدخلات، إذا كانت عقدة "UNTIL*"، سيخرج:

u,u,u,u,v,v,...

السبب الذي يجعلني أفرق حتى مع علامة النجمة هو بيت القصيد من السؤال، "u UNTIL* v" يكون صحيحًا فقط عندما يتم أخذ v كإخراج بمجرد ظهوره في الدفق الثاني، وهو أثر واحد يرضي "u UNTIL* v" نظرًا لـ إشارات الإدخال. كيف نعبر عن هذا القيد ؟!يبدو LTL عامًا جدًا بالنسبة إلى "آلية فرض القيد" هذه.

ملحوظة:من فضلك تحملني، أنا لست عالم كمبيوتر ولا عالم رياضيات، أنا مبرمج عادي يحاول تعلم أشياء جديدة.

Answer 1

هذا سؤال جيد.

إنه ليس سؤال LTL (المنطق الزمني الخطي) بشكل مباشر - بل هو سؤال حول ما إذا كانت هناك خوارزمية أو أداة تأخذ تدفق الإدخال وتعديله بطريقة بسيطة إلى حد ما لتلبية خاصية LTL معينة.

ما إذا كان ما تريده يمكن القيام به أو تم القيام به يعتمد على ما هي التعديلات المسموح بها على الدفق بالضبط.في المثال الخاص بك، أنت، بمعنى ما، تقوم بإعادة مزج تيارين.لاحظ أن LTL يتم تعريفه عبر الحروف الهجائية حيث يمكن أن يحتوي كل حرف على افتراضات متعددة تكون صحيحة في ذلك الوقت.لذا، في مثالك، كان بإمكانك خلط مجرى u وv معًا للحصول على:

u,u,u,u,{u,v},{u,v},....

وهذا من شأنه أن يرضي صيغة LTL أيضًا.إذا كانت الطريقة التي تقوم بها بإعادة المزج هي أن الاقتراح في تدفق الإخراج هو دائمًا مجموعة فرعية من الاقتراحات المحددة في تدفق الإدخال، فيمكنك استخدام التوليف التفاعلي للحصول على محول طاقة يقوم بخلط/تثبيت التيار.ومع ذلك، لن ينجح هذا إلا إذا كان هناك طريقة فعلية لإجراء المزج لكل دفق إخراج.

إذا كان هناك فكرة كمية عن الخلط/التثبيت، فقد يكون التوليف الكمي مجالًا بحثيًا قد يكون له بعض النتائج.ولكنك ستحتاج إلى وصف لمعيار تحسين تعديل الدفق الدقيق لمعرفة ما إذا كانت أي من النتائج من تلك المنطقة قابلة للتطبيق.